VERS5 
NIL 
((EPSILONDEF SETS#4) (SET_EXTENSIONALITY SETS#5) (CHOICE SETS#9) (DEMORGAN NORMAL#5) (DEMORGAN1 NORMAL#6) (EXCLUDED_MIDDLE NORMAL#7) (TRANS_COND NORMAL#8) (DISJUNCT_SUBST NORMAL#9) (INCONSISTENT NORMAL#10) (ZERO_NOT_SUCCESSOR NATNUM#6) (SUCCESSOREQ NATNUM#7) (PROOF_BY_INDUCTION NATNUM#8) (LANDAU_TH1 NATNUM#9) (LANDAU_TH2 NATNUM#10) (LANDAU_TH3 NATNUM#11) (LANDAU_TH4 NATNUM#15) (COMMUTADD NATNUM#17) (LANDAU_TH7 NATNUM#18) (LANDAU_TH8 NATNUM#19) (TRCT0 NATNUM#20) (TRCT1 NATNUM#21) (TRCT2 NATNUM#22) (TRCT3 NATNUM#23) (PLUSDEF1 NATNUM#24) (LPLUSCAN NATNUM#26) (RPLUSCAN NATNUM#27) (ADDTOZERO NATNUM#28) (LANDAU_DEF2 ORDERING#3) (TOTALORD ORDERING#5) (STRICT1 ORDERING#6) (STRICT2 ORDERING#7) (STRICT3 ORDERING#8) (GREATERP_LESSP ORDERING#9) (GRTEQP_LSSEQP ORDERING#14) (TRANSITIVITY_OF_ORDER ORDERING#15) (TRANSITIVITY_OF_GREATERP ORDERING#16) (LSSEQP_LESSP_LESSP ORDERING#17) (LESSP_LSSEQP_LESSP ORDERING#18) (TRANSITIVITY_OF_LSSEQP ORDERING#19) (INCREASING ORDERING#20) (SUCCESSORLESS ORDERING#21) (RPLUS_GREATCAN ORDERING#22) (RPLUS_LESSCAN ORDERING#23) (LANDAU_TH21 ORDERING#24) (LANDAU_A_TH22 ORDERING#25) (LANDAU_B_TH22 ORDERING#26) (LANDAU_TH23 ORDERING#27) (LANDAU_A_TH24 ORDERING#28) (ZEROLEAST1 ORDERING#29) (ZEROLEAST2 ORDERING#30) (LANDAU_B_TH24 ORDERING#31) (LANDAU_TH25 ORDERING#32) (LANDAU_TH26 ORDERING#33) (LANDAU_TH27 ORDERING#34) (LANDAU_DEF6 MULTIP#2) (TIMSUCC MULTIP#5) (LTIMESCAN MULTIP#6) (RTIMESCAN MULTIP#7) (COMMUTMULT MULTIP#8) (LTIMESTOZERO MULTIP#9) (RTIMESTOZERO MULTIP#10) (NOZERODIVISORS MULTIP#11) (TIMESFACT MULTIP#11) (LDISTRIB MULTIP#12) (RDISTRIB MULTIP#13) (LANDAU_A_TH32 MULTIP#14) (LANDAU_D_TH32 MULTIP#15) (LANDAU_A_TH33 MULTIP#16) (LANDAU_B_TH33 MULTIP#17) (LANDAU_C_TH33 MULTIP#18) (LANDAU_TH34 MULTIP#19) (LANDAU_A_TH35 MULTIP#20) (LANDAU_B_TH35 MULTIP#21) (LANDAU_TH36 MULTIP#22) (ALLDEF ALL#3) (SOMEDEF ALL#4) (ALLFACT ALL#5) (SOMEFACT ALL#6) (LISTINDUCTION LISPAX#30) (LISTINDUCTIONDEF LISPAX#34) (SEXPINDUCTION LISPAX#35) (SEXPINDUCTIONDEF LISPAX#36) (HIGH_ORDER_DEFINITION LISPAX#40) (LISTDEF LISPAX#45) (APPENDEF LISPAX#47) (LISTAPPEND LISPAX#48) (ALLPDEF LISPAX#52) (SOMEPDEF LISPAX#53) (MAPCARDEF LISPAX#54) (ALISTDEF1 LISPAX#57) (ALISTDEF LISPAX#58) (ASSOCDEF LISPAX#60) (MEMBERDEF LISPAX#63) (UNIQUENESSDEF LISPAX#65) (PAIRING LISPAX#72) (FRACT0 FRACTIONS#3) (FRACT1 FRACTIONS#4) (FRACT2 FRACTIONS#5) (FRACT4 FRACTIONS#6) (EFDEF FRACTIONS#8) (FRACT3 FRACTIONS#9) (REFLEXF FRACTIONS#10) (SYMMF FRACTIONS#11) (TRANSF FRACTIONS#12) (TRANSF1 FRACTIONS#13) (FR_EQCLASS FRACTIONS#14) (TOTALORDFR FRORDERING#5) (STRICTFR1 FRORDERING#6) (ANTISYMLESS FRORDERING#6) (STRICTLYLESS FRORDERING#6) (STRICTFR2 FRORDERING#7) (STRICTFR3 FRORDERING#8) (GF_LF FRORDERING#9) (EF_LF FRORDERING#10) (LF_EF FRORDERING#11) (LF_EF_EF_LF FRORDERING#12) (GF_EF_EF_GF FRORDERING#13) (GEFDEF FRORDERING#15) (LEFDEF FRORDERING#17) (LANDAU_TH46 FRORDERING#18) (LANDAU_TH47 FRORDERING#19) (GEF_LEF FRORDERING#20) (TRANSORDFR FRORDERING#21) (LANDAU_A_TH51 FRORDERING#22) (LANDAU_B_TH51 FRORDERING#23) (LANDAU_TH52 FRORDERING#24) (NOLASTFR FRORDERING#25) (NOLEASTFR FRORDERING#26) (DENSEFR FRORDERING#27) (QZEROPDEF FRORDERING#30) (QZEROLEAST2 FRORDERING#31) (PLUSFDEF FRACTSUM#2) (PLUSFSORT FRACTSUM#3) (SUMF_UNIQUENESS FRACTSUM#4) (SUMF_SIMPL FRACTSUM#5) (COMMUTFADD FRACTSUM#6) (ASSOCFADD FRACTSUM#7) (SUMF_INCREASING FRACTSUM#8) (LF_SUMFPRESERV FRACTSUM#9) (EF_SUMFPRESERV FRACTSUM#10) (GF_SUMFPRESERV FRACTSUM#11) (GF_SUMFSIMPL FRACTSUM#12) (EF_SUMFSIMPL FRACTSUM#13) (LF_SUMFSIMPL FRACTSUM#14) (GF_GF_SUMFPRESERV FRACTSUM#15) (LEF_LF_SUMFPRESERV FRACTSUM#16) (LF_LEF_SUMFPRESERV FRACTSUM#17) (LEF_LEF_SUMFPRESERV FRACTSUM#18) (PLUS_QZERO FRACTSUM#19) (MINUSDEF FRACTSUM#20) (MINUSDEFINITION FRACTSUM#21) (TIMESFDEF FRACTMULT#2) (PRODF_UNIQUENESS FRACTMULT#4) (COMMUTFPROD FRACTMULT#5) (ASSOCFPROD FRACTMULT#6) (DISTRIBF_LEFT FRACTMULT#7) (GF_PRODFPRESERV FRACTMULT#8) (EF_PRODFPRESERV FRACTMULT#9) (LF_PRODFPRESERV FRACTMULT#10) (GF_PRODFSIMPL FRACTMULT#11) (EF_PRODFSIMPL FRACTMULT#12) (LF_PRODFSIMPL FRACTMULT#13) (GF_GF_PRODFPRESERV FRACTMULT#14) (LEF_LF_PRODFPRESERV FRACTMULT#15) (LF_LEF_PRODFPRESERV FRACTMULT#16) (LEF_LEF_PRODFPRESERV FRACTMULT#17) (INVDEF FRACTMULT#18) (INVSORT FRACTMULT#19) (RTIMES_QONE FRACTMULT#20) (LTIMES_QONE FRACTMULT#21) (FIELD FRACTMULT#22) (TFZF FRACTMULT#23) (DIVISION FRACTMULT#24) (DIVISIONDEFINITION FRACTMULT#25) (CONS_CAR_CDR LISPAX#28 LISPAX#29) (NORMAL NORMAL#1 NORMAL#2 NORMAL#3 NORMAL#4) (TRICOTOMY NATNUM#20 NATNUM#21 NATNUM#22 NATNUM#23) (SUCCFACTS NATNUM#6 NATNUM#7 ORDERING#21 ORDERING#29 ORDERING#30) (TIMESFACTS MULTIP#2 MULTIP#4 MULTIP#5 MULTIP#6 MULTIP#7 MULTIP#8 MULTIP#9 MULTIP#10 MULTIP#12 MULTIP#13) (PLUSFACTS NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#22 ORDERING#23 MULTIP#12 MULTIP#13) (SIMPINFO NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19 FRACTMULT#3 FRACTMULT#19)) (NIL . (DECL (ARB ARB1 ARB2) (TYPE: (TY& . ?ARBITRARY))) . ((ARB2 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#1 . NIL . VARIABLE .)) (ARB1 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#1 . NIL . VARIABLE .)) (ARB . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#1 . NIL . VARIABLE .))) . NIL . NIL . NIL . SETS . NIL . 1 .)(NIL . (DECL (SETVAR SETVAR1) (TYPE: (TY& . |(?ARBITRARY)→TRUTHVAL|))) . ((SETVAR1 . (|(?ARBITRARY)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#2 . NIL . VARIABLE .)) (SETVAR . (|(?ARBITRARY)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#2 . NIL . VARIABLE .))) . NIL . NIL . NIL . SETS . NIL . 2 .)(|∀P P1 P2.(P∨P1)∧P2≡P∧P2∨P1∧P2| . (AXIOM (TM& . |∀P P1 P2.(P∨P1)∧P2≡P∧P2∨P1∧P2|)) . ((P2 . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#1 . NIL . VARIABLE .)) (P1 . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#1 . NIL . VARIABLE .)) (P . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NORMAL#1 . NIL . VARIABLE .))) . NIL . (NORMAL#1) . NIL . NORMAL . NIL . 1 .)(NIL . (DECL (I J K N M) (SORT: (TM& . NATNUM)) (TYPE: (TY& . GROUND))) . ((M . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#1 . NIL . VARIABLE .)) (N . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#1 . NIL . VARIABLE .)) (K . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#1 . NIL . VARIABLE .)) (J . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#1 . NIL . VARIABLE .)) (I . (GROUND . (SYMBOL& NATNUM NIL) . NIL . NIL . NATNUM#1 . NIL . VARIABLE .))) . NIL . NIL . NIL . NATNUM . NIL . 1 .)(NIL . (DECL (A B C SET) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((SET . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#2 . NIL . VARIABLE .)) (C . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#2 . NIL . VARIABLE .)) (B . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#2 . NIL . VARIABLE .)) (A . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . NATNUM#2 . NIL . VARIABLE .))) . NIL . NIL . NIL . NATNUM . NIL . 2 .)(NIL . (DECL ADD1 (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (POSTFIXNAME: /') (BINDINGPOWER: 975)) . ((ADD1 . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 975) (POSTFIX& . /')) . NATNUM#3 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 3 .)(|NATNUM(0)| . (TRW (TM& . |NATNUM(0)|) NIL) . NIL . NIL . NIL . NIL . NATNUM . NIL . 4 .)(NIL . (DECL LESSP (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT) (INFIXNAME: <) (BINDINGPOWER: 920)) . ((LESSP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . <)) . ORDERING#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . ORDERING . NIL . 1 .)(NIL . (DECL GREATERP (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT) (INFIXNAME: >) (BINDINGPOWER: 920)) . ((GREATERP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . >)) . ORDERING#2 . NIL . CONSTANT .))) . NIL . NIL . NIL . ORDERING . NIL . 2 .)(NIL . (DECL TIMES (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (INFIXNAME: *) (ASSOCIATIVITY: BOTH) (BINDINGPOWER: 935)) . ((TIMES . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 935) (INFIX& . *)) . MULTIP#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . MULTIP . NIL . 1 .)(NIL . (DECL CAR (UNARYNAME: CAR) (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((CAR . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 950) (UNARY& . CAR)) . LISPAX#1 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 1 .)(NIL . (DECL CDR (UNARYNAME: CDR) (TYPE: (TY& . GROUND→GROUND)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 950)) . ((CDR . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 950) (UNARY& . CDR)) . LISPAX#2 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 2 .)(NIL . (DECL ATOM (UNARYNAME: ATOM) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((ATOM . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . ATOM)) . LISPAX#3 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 3 .)(NIL . (DECL NULL (UNARYNAME: NULL) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((NULL . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . NULL)) . LISPAX#4 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 4 .)(NIL . (DECL LISTP (UNARYNAME: LISTP) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((LISTP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . LISTP)) . LISPAX#5 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 5 .)(NIL . (DECL ALISTP (UNARYNAME: ALISTP) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((ALISTP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . ALISTP)) . LISPAX#6 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 6 .)(NIL . (DECL SEXP (UNARYNAME: SEXP) (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT) (BINDINGPOWER: 750)) . ((SEXP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 750) (UNARY& . SEXP)) . LISPAX#7 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 7 .)(NIL . (DECL (Q Q0 Q1 Q2 Q3 Q01 Q02 Q03) (TYPE: (TY& . GROUND)) (SORT: (TM& . FR))) . ((Q03 . (GROUND . (SYMBOL& FR NIL) . NIL . NIL . FRACTIONS#1 . NIL . VARIABLE .)) (Q02 . (GROUND . (SYMBOL& FR NIL) . NIL . NIL . FRACTIONS#1 . NIL . VARIABLE .)) (Q01 . (GROUND . (SYMBOL& FR NIL) . NIL . NIL . FRACTIONS#1 . NIL . VARIABLE .)) (Q3 . (GROUND . (SYMBOL& FR NIL) . NIL . NIL . FRACTIONS#1 . NIL . VARIABLE .)) (Q2 . (GROUND . (SYMBOL& FR NIL) . NIL . NIL . FRACTIONS#1 . NIL . VARIABLE .)) (Q1 . (GROUND . (SYMBOL& FR NIL) . NIL . NIL . FRACTIONS#1 . NIL . VARIABLE .)) (Q0 . (GROUND . (SYMBOL& FR NIL) . NIL . NIL . FRACTIONS#1 . NIL . VARIABLE .)) (Q . (GROUND . (SYMBOL& FR NIL) . NIL . NIL . FRACTIONS#1 . NIL . VARIABLE .)) (FR . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRACTIONS#1 . NIL . VARIABLE .))) . NIL . NIL . NIL . FRACTIONS . NIL . 1 .)(NIL . (DECL EPSILON (TYPE: (TY& . |((@ARB)⊗(@SETVAR))→TRUTHVAL|)) (INFIXNAME: ε) (BINDINGPOWER: 925)) . ((EPSILON . (|((@ARB)⊗(@SETVAR))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 925) (INFIX& . ε)) . SETS#3 . NIL . VARIABLE .)) SETVAR ARB) . NIL . NIL . NIL . SETS . NIL . 3 .)(|∀ARB1 OBJ1.ARB1εOBJ1≡OBJ1(ARB1)| . (DEFINE EPSILON (TM& . |∀ARB1 OBJ1.ARB1εOBJ1≡OBJ1(ARB1)|) NIL) . ((EPSILON . (|((@ARB)⊗(@SETVAR))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 925) (INFIX& . ε)) . SETS#4 . NIL . DEFINED .)) ARB2 ARB1 ARB SETVAR (OBJ1 . (|(?ARBITRARY)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#4 . NIL . VARIABLE .))) . NIL . (SETS#4) . NIL . SETS . NIL . 4 .)(|∀P P1 P2.P2∧(P∨P1)≡P2∧P∨P2∧P1| . (AXIOM (TM& . |∀P P1 P2.P2∧(P∨P1)≡P2∧P∨P2∧P1|)) . (P2 P1 P) . NIL . (NORMAL#2) . NIL . NORMAL . NIL . 2 .)(|∀P P1 P2.P2∧(P∨P1)≡P∧P2∨P1∧P2| . (AXIOM (TM& . |∀P P1 P2.P2∧(P∨P1)≡P∧P2∨P1∧P2|)) . (P2 P1 P) . NIL . (NORMAL#3) . NIL . NORMAL . NIL . 3 .)(|∀P P1 P2.(P∨P1⊃P2)≡(P⊃P2)∧(P1⊃P2)| . (AXIOM (TM& . |∀P P1 P2.(P∨P1⊃P2)≡(P⊃P2)∧(P1⊃P2)|)) . (P2 P1 P) . NIL . (NORMAL#4) . NIL . NORMAL . NIL . 4 .)(|∀P P1.¬(P∨P1)≡¬P∧¬P1| . (AXIOM (TM& . |∀P P1.¬(P∨P1)≡¬P∧¬P1|)) . (P2 P1 P) . NIL . (NORMAL#5) . NIL . NORMAL . NIL . 5 .)(|∀P P1.¬(P∧P1)≡¬P∨¬P1| . (AXIOM (TM& . |∀P P1.¬(P∧P1)≡¬P∨¬P1|)) . (P2 P1 P) . NIL . (NORMAL#6) . NIL . NORMAL . NIL . 6 .)(|∀P P1.P≡(P1⊃P)∧(¬P1⊃P)| . (AXIOM (TM& . |∀P P1.P≡(P1⊃P)∧(¬P1⊃P)|)) . (P2 P1 P) . NIL . (NORMAL#7) . NIL . NORMAL . NIL . 7 .)(|∀P P1 P2.(P1⊃P2)∧(IF P THEN P1 ELSE P2)⊃P2| . (AXIOM (TM& . |∀P P1 P2.(P1⊃P2)∧(IF P THEN P1 ELSE P2)⊃P2|)) . (P2 P1 P) . NIL . (NORMAL#8) . NIL . NORMAL . NIL . 8 .)(|∀P1 P2 P3 P4.(P2≡P4)∧(P1∨P2∨P3)⊃P1∨P4∨P3| . (AXIOM (TM& . |∀P1 P2 P3 P4.(P2≡P4)∧(P1∨P2∨P3)⊃P1∨P4∨P3|)) . (P2 P1 P (P4 . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 1000)) . NORMAL#9 . NIL . VARIABLE .)) (P3 . (TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 1000)) . NORMAL#9 . NIL . VARIABLE .))) . NIL . (NORMAL#9) . NIL . NORMAL . NIL . 9 .)(|∀P P1 P2.P∧P1⊃¬P2≡¬(P∧P1∧P2)| . (AXIOM (TM& . |∀P P1 P2.P∧P1⊃¬P2≡¬(P∧P1∧P2)|)) . (P2 P1 P) . NIL . (NORMAL#10) . NIL . NORMAL . NIL . 10 .)(|∀N.NATNUM(N')| . (AXIOM (TM& . |∀N.NATNUM(N')|)) . (M N K J I ADD1) . NIL . (NATNUM#5) . NIL . NATNUM . NIL . 5 .)(|∀N.¬N'=0| . (AXIOM (TM& . |∀N.¬N'=0|)) . (M N K J I ADD1) . NIL . (NATNUM#6) . NIL . NATNUM . NIL . 6 .)(|∀N M.N'=M'≡N=M| . (AXIOM (TM& . |∀N M.N'=M'≡N=M|)) . (M N K J I ADD1) . NIL . (NATNUM#7) . NIL . NATNUM . NIL . 7 .)(|∀A.A(0)∧(∀N.A(N)⊃A(N'))⊃(∀N.A(N))| . (AXIOM (TM& . |∀A.A(0)∧(∀N.A(N)⊃A(N'))⊃(∀N.A(N))|)) . (M N K J I SET C B A ADD1) . NIL . (NATNUM#8) . NIL . NATNUM . NIL . 8 .)(NIL . (DECL ALL (TYPE: (TY& . |(GROUND⊗(@SET))→TRUTHVAL|)) (SYNTYPE: CONSTANT)) . ((ALL . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ALL#1 . NIL . CONSTANT .)) SET) . NIL . NIL . NIL . ALL . NIL . 1 .)(NIL . (DECL SOME (TYPE: (TY& . |(GROUND⊗(@SET))→TRUTHVAL|)) (SYNTYPE: CONSTANT)) . ((SOME . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ALL#2 . NIL . CONSTANT .)) SET) . NIL . NIL . NIL . ALL . NIL . 2 .)(|∀N A.ALL(0,A)∧(ALL(N',A)≡A(N)∧ALL(N,A))| . (DEFAX ALL (TM& . |∀N A.ALL(0,A)∧(ALL(N',A)≡A(N)∧ALL(N,A))|)) . ((ALL . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ALL#3 . NIL . DEFINED .)) M N K J I SET C B A ADD1) . NIL . (ALL#3) . NIL . ALL . NIL . 3 .)(|∀N A.¬SOME(0,A)∧(SOME(N',A)≡A(N)∨SOME(N,A))| . (DEFAX SOME (TM& . |∀N A.¬SOME(0,A)∧(SOME(N',A)≡A(N)∨SOME(N,A))|)) . ((SOME . (|(GROUND⊗(@SET))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . ALL#4 . NIL . DEFINED .)) M N K J I SET C B A ADD1) . NIL . (ALL#4) . NIL . ALL . NIL . 4 .)(NIL . (DECL (U V W) (TYPE: (TY& . GROUND)) (SORT: (TM& . LISTP))) . ((W . (GROUND . (SYMBOL& LISTP NIL) . NIL . NIL . LISPAX#8 . NIL . VARIABLE .)) (V . (GROUND . (SYMBOL& LISTP NIL) . NIL . NIL . LISPAX#8 . NIL . VARIABLE .)) (U . (GROUND . (SYMBOL& LISTP NIL) . NIL . NIL . LISPAX#8 . NIL . VARIABLE .)) LISTP) . NIL . NIL . NIL . LISPAX . NIL . 8 .)(NIL . (DECL (X Y Z) (TYPE: (TY& . GROUND)) (SORT: (TM& . SEXP))) . ((Z . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . LISPAX#9 . NIL . VARIABLE .)) (Y . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . LISPAX#9 . NIL . VARIABLE .)) (X . (GROUND . (SYMBOL& SEXP NIL) . NIL . NIL . LISPAX#9 . NIL . VARIABLE .)) SEXP) . NIL . NIL . NIL . LISPAX . NIL . 9 .)(NIL . (DECL (XA YA ZA) (TYPE: (TY& . GROUND)) (SORT: (TM& . ATOM))) . ((ZA . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . LISPAX#10 . NIL . VARIABLE .)) (YA . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . LISPAX#10 . NIL . VARIABLE .)) (XA . (GROUND . (SYMBOL& ATOM NIL) . NIL . NIL . LISPAX#10 . NIL . VARIABLE .)) ATOM) . NIL . NIL . NIL . LISPAX . NIL . 10 .)(NIL . (DECL (PHI) (TYPE: (TY& . GROUND→TRUTHVAL))) . ((PHI . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#11 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 11 .)(NIL . (DECL CONS (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|)) (SYNTYPE: CONSTANT) (INFIXNAME: |.|) (PREFIXNAME: CONS) (BINDINGPOWER: 850)) . ((CONS . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 850) (PREFIX& . CONS) (INFIX& . |.|)) . LISPAX#12 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 12 .)(|∀Q.LISTP Q| . (AXIOM (TM& . |∀Q.LISTP Q|)) . (LISTP FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q) . NIL . (FRACTIONS#2) . NIL . FRACTIONS . NIL . 2 .)(NIL . (DECL GF (TYPE: (TY& . |((@Q)⊗(@Q))→TRUTHVAL|))) . ((GF . (|((@Q)⊗(@Q))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRORDERING#1 . NIL . VARIABLE .)) Q) . NIL . NIL . NIL . FRORDERING . NIL . 1 .)(NIL . (DECL PF (TYPE: (TY& . |((@Q)⊗(@Q))→(@Q)|)) (BINDINGPOWER: 940)) . ((PF . (|((@Q)⊗(@Q))→(@Q)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 940)) . FRACTSUM#1 . NIL . VARIABLE .)) Q) . NIL . NIL . NIL . FRACTSUM . NIL . 1 .)(NIL . (DECL TF (TYPE: (TY& . |((@Q)⊗(@Q))→(@Q)|)) (BINDINGPOWER: 935)) . ((TF . (|((@Q)⊗(@Q))→(@Q)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 935)) . FRACTMULT#1 . NIL . VARIABLE .)) Q) . NIL . NIL . NIL . FRACTMULT . NIL . 1 .)(|∀SETVAR SETVAR1.(∀ARB.ARBεSETVAR≡ARBεSETVAR1)⊃SETVAR=SETVAR1| . (AXIOM (TM& . |∀SETVAR SETVAR1.(∀ARB.ARBεSETVAR≡ARBεSETVAR1)⊃SETVAR=SETVAR1|)) . (ARB2 ARB1 ARB SETVAR1 SETVAR EPSILON OBJ1) . NIL . (SETS#5) . NIL . SETS . NIL . 5 .)(NIL . (DECL FUNCTION (TYPE: (TY& . |((?ARBITRARY)*)→(?ARBITRARY)|)) (SYNTYPE: VARIABLE)) . ((FUNCTION . (|((?ARBITRARY)*)→(?ARBITRARY)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#6 . NIL . VARIABLE .))) . NIL . NIL . NIL . SETS . NIL . 6 .)(NIL . (DECL ZETA (TYPE: (TY& . |((?ARBITRARY)*)→TRUTHVAL|)) (SYNTYPE: VARIABLE)) . ((ZETA . (|((?ARBITRARY)*)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#7 . NIL . VARIABLE .))) . NIL . NIL . NIL . SETS . NIL . 7 .)(NIL . (DECL PARVAR (TYPE: (TY& . ?ARBITRARY)) (SYNTYPE: VARIABLE)) . ((PARVAR . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . SETS#8 . NIL . VARIABLE .))) . NIL . NIL . NIL . SETS . NIL . 8 .)(|∀M N.¬M=N⊃¬M'=N'| . (DERIVE (TM& . |∀M N.¬M=N⊃¬M'=N'|) ((LR& NATNUM#7)) NIL) . (M N K J I ADD1) . NIL . (NATNUM#5 NATNUM#6 NATNUM#7) . NIL . NATNUM . NIL . 9 .)(|∀N.¬N=N'| . (UE (UELST& (A . |λN.¬N=N'|)) (LN& . NATNUM#8) (USE (LR& NATNUM#7))) . (M N K J I SET C B A ADD1) . NIL . (NATNUM#8 NATNUM#5 NATNUM#6 NATNUM#7) . NIL . NATNUM . NIL . 10 .)(|∀N.¬N=0⊃(∃K.N=K')| . (UE (UELST& (A . |λN.¬N=0⊃(∃K.N=K')|)) (LN& . NATNUM#8) NIL) . (M N K J I SET C B A ADD1) . NIL . (NATNUM#8 NATNUM#5 NATNUM#6 NATNUM#7) . NIL . NATNUM . NIL . 11 .)(NIL . (DECL PLUS (INFIXNAME: +) (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (ASSOCIATIVITY: BOTH) (BINDINGPOWER: 930)) . ((PLUS . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 930) (INFIX& . +)) . NATNUM#12 . NIL . CONSTANT .))) . NIL . NIL . NIL . NATNUM . NIL . 12 .)(|∀N K.0+N=N∧K'+N=(K+N)'| . (DEFAX PLUS (TM& . |∀N K.0+N=N∧K'+N=(K+N)'|)) . ((PLUS . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 930) (INFIX& . +)) . NATNUM#13 . NIL . DEFINED .)) M N K J I ADD1) . NIL . (NATNUM#13) . NIL . NATNUM . NIL . 13 .)(|∀XA.SEXP XA| . (AXIOM (TM& . |∀XA.SEXP XA|)) . (ATOM SEXP ZA YA XA) . NIL . (LISPAX#13) . NIL . LISPAX . NIL . 13 .)(|∀U.SEXP U| . (AXIOM (TM& . |∀U.SEXP U|)) . (LISTP SEXP W V U) . NIL . (LISPAX#14) . NIL . LISPAX . NIL . 14 .)(|∀X U.LISTP X.U| . (AXIOM (TM& . |∀X U.LISTP X.U|)) . (LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#15) . NIL . LISPAX . NIL . 15 .)(|∀U.¬NULL U⊃LISTP CDR U| . (AXIOM (TM& . |∀U.¬NULL U⊃LISTP CDR U|)) . (CDR NULL LISTP W V U) . NIL . (LISPAX#16) . NIL . LISPAX . NIL . 16 .)(|∀U.¬NULL U⊃SEXP CAR U| . (AXIOM (TM& . |∀U.¬NULL U⊃SEXP CAR U|)) . (CAR NULL LISTP SEXP W V U) . NIL . (LISPAX#17) . NIL . LISPAX . NIL . 17 .)(|∀X.¬ATOM X⊃SEXP CAR X| . (AXIOM (TM& . |∀X.¬ATOM X⊃SEXP CAR X|)) . (CAR ATOM SEXP Z Y X) . NIL . (LISPAX#18) . NIL . LISPAX . NIL . 18 .)(|∀X.¬ATOM X⊃SEXP CDR X| . (AXIOM (TM& . |∀X.¬ATOM X⊃SEXP CDR X|)) . (CDR ATOM SEXP Z Y X) . NIL . (LISPAX#19) . NIL . LISPAX . NIL . 19 .)(|∀X Y.SEXP X.Y| . (AXIOM (TM& . |∀X Y.SEXP X.Y|)) . (SEXP Z Y X CONS) . NIL . (LISPAX#20) . NIL . LISPAX . NIL . 20 .)(|∀X Y.¬ATOM X.Y| . (AXIOM (TM& . |∀X Y.¬ATOM X.Y|)) . (ATOM SEXP Z Y X CONS) . NIL . (LISPAX#21) . NIL . LISPAX . NIL . 21 .)(|∀X U.¬NULL X.U| . (AXIOM (TM& . |∀X U.¬NULL X.U|)) . (NULL LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#22) . NIL . LISPAX . NIL . 22 .)(|∀U.NULL U⊃U=NIL| . (AXIOM (TM& . |∀U.NULL U⊃U=NIL|)) . (NULL LISTP W V U) . NIL . (LISPAX#23) . NIL . LISPAX . NIL . 23 .)(|∀X Y.CAR (X.Y)=X| . (AXIOM (TM& . |∀X Y.CAR (X.Y)=X|)) . (CAR SEXP Z Y X CONS) . NIL . (LISPAX#24) . NIL . LISPAX . NIL . 24 .)(|∀X Y.CDR (X.Y)=Y| . (AXIOM (TM& . |∀X Y.CDR (X.Y)=Y|)) . (CDR SEXP Z Y X CONS) . NIL . (LISPAX#25) . NIL . LISPAX . NIL . 25 .)(|CAR NIL=NIL| . (AXIOM (TM& . |CAR NIL=NIL|)) . (CAR) . NIL . (LISPAX#26) . NIL . LISPAX . NIL . 26 .)(|CDR NIL=NIL| . (AXIOM (TM& . |CDR NIL=NIL|)) . (CDR) . NIL . (LISPAX#27) . NIL . LISPAX . NIL . 27 .)(|∀U.¬NULL U⊃CAR U.CDR U=U| . (AXIOM (TM& . |∀U.¬NULL U⊃CAR U.CDR U=U|)) . (CAR CDR NULL LISTP W V U CONS) . NIL . (LISPAX#28) . NIL . LISPAX . NIL . 28 .)(|∀X.¬ATOM X⊃CAR X.CDR X=X| . (AXIOM (TM& . |∀X.¬ATOM X⊃CAR X.CDR X=X|)) . (CAR CDR ATOM SEXP Z Y X CONS) . NIL . (LISPAX#29) . NIL . LISPAX . NIL . 29 .)(|∀PHI.PHI(NIL)∧(∀X U.PHI(U)⊃PHI(X.U))⊃(∀U.PHI(U))| . (AXIOM (TM& . |∀PHI.PHI(NIL)∧(∀X U.PHI(U)⊃PHI(X.U))⊃(∀U.PHI(U))|)) . (LISTP SEXP W V U Z Y X PHI CONS) . NIL . (LISPAX#30) . NIL . LISPAX . NIL . 30 .)(NIL . (DECL PARS (TYPE: (TY& . GROUND*))) . ((PARS . (GROUND* . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#31 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 31 .)(NIL . (DECL (DF DF1 DF2) (TYPE: (TY& . |(GROUND⊗(GROUND*))→(GROUND*)|))) . ((DF2 . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#32 . NIL . VARIABLE .)) (DF1 . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#32 . NIL . VARIABLE .)) (DF . (|(GROUND⊗(GROUND*))→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#32 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 32 .)(NIL . (DECL NILCASE (TYPE: (TY& . |(GROUND*)→(GROUND*)|))) . ((NILCASE . (|(GROUND*)→(GROUND*)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#33 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 33 .)(|(∀ARB1.(∃ARB2.ZETA(ARB1,ARB2,PARVAR)))⊃(∃FUNCTION.(∀ARB1.ZETA(ARB1,FUNCTION(ARB1,PARVAR),PARVAR)))| . (AXIOM (TM& . |(∀ARB1.(∃ARB2.ZETA(ARB1,ARB2,PARVAR)))⊃(∃FUNCTION.(∀ARB1.ZETA(ARB1,FUNCTION(ARB1,PARVAR),PARVAR)))|)) . (ARB2 ARB1 ARB FUNCTION ZETA PARVAR) . NIL . (SETS#9) . NIL . SETS . NIL . 9 .)(|∀N M.NATNUM(N+M)| . (AXIOM (TM& . |∀N M.NATNUM(N+M)|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#14) . NIL . NATNUM . NIL . 14 .)(|∀N M.(∃K.K=N+M∧(∀I J.I=M+N∧J=M+N⊃I=J))| . (AXIOM (TM& . |∀N M.(∃K.K=N+M∧(∀I J.I=M+N∧J=M+N⊃I=J))|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#15) . NIL . NATNUM . NIL . 15 .)(|∀N.N+0=N| . (AXIOM (TM& . |∀N.N+0=N|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#16) . NIL . NATNUM . NIL . 16 .)(|∀K N.K+N=N+K| . (AXIOM (TM& . |∀K N.K+N=N+K|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#17) . NIL . NATNUM . NIL . 17 .)(|∀N M.¬N=N+M'| . (AXIOM (TM& . |∀N M.¬N=N+M'|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#18) . NIL . NATNUM . NIL . 18 .)(|∀N K M.¬K=M⊃¬N+K=N+M| . (AXIOM (TM& . |∀N K M.¬K=M⊃¬N+K=N+M|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#19) . NIL . NATNUM . NIL . 19 .)(|∀N M.M=N∨(∃K.M=N+K')∨(∃K.N=M+K')| . (AXIOM (TM& . |∀N M.M=N∨(∃K.M=N+K')∨(∃K.N=M+K')|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#20) . NIL . NATNUM . NIL . 20 .)(|∀N M.M=N⊃¬(∃K.M=N+K')∧¬(∃K.N=M+K')| . (AXIOM (TM& . |∀N M.M=N⊃¬(∃K.M=N+K')∧¬(∃K.N=M+K')|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#21) . NIL . NATNUM . NIL . 21 .)(|∀N M.(∃K.M=N+K')⊃¬M=N∧¬(∃K.N=M+K')| . (AXIOM (TM& . |∀N M.(∃K.M=N+K')⊃¬M=N∧¬(∃K.N=M+K')|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#22) . NIL . NATNUM . NIL . 22 .)(|∀N M.(∃K.N=M+K')⊃¬M=N∧¬(∃K.M=N+K')| . (AXIOM (TM& . |∀N M.(∃K.N=M+K')⊃¬M=N∧¬(∃K.M=N+K')|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#23) . NIL . NATNUM . NIL . 23 .)(|∀N.1+N=N'∧N+1=N'| . (AXIOM (TM& . |∀N.1+N=N'∧N+1=N'|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#24) . NIL . NATNUM . NIL . 24 .)(|∀N K.N+K'=(N+K)'| . (AXIOM (TM& . |∀N K.N+K'=(N+K)'|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#25) . NIL . NATNUM . NIL . 25 .)(|∀N K M.K+M=K+N≡M=N| . (AXIOM (TM& . |∀N K M.K+M=K+N≡M=N|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#26) . NIL . NATNUM . NIL . 26 .)(|∀N K M.M+K=N+K≡M=N| . (AXIOM (TM& . |∀N K M.M+K=N+K≡M=N|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#27) . NIL . NATNUM . NIL . 27 .)(|∀N K.N+K=0≡N=0∧K=0| . (AXIOM (TM& . |∀N K.N+K=0≡N=0∧K=0|)) . (M N K J I ADD1 PLUS) . NIL . (NATNUM#28) . NIL . NATNUM . NIL . 28 .)(|∀N M.N>M≡(∃K.N=M+K')| . (DEFAX GREATERP (TM& . |∀N M.N>M≡(∃K.N=M+K')|)) . ((GREATERP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . >)) . ORDERING#3 . NIL . DEFINED .)) M N K J I ADD1 PLUS) . NIL . (ORDERING#3) . NIL . ORDERING . NIL . 3 .)(|∀N M.N<M≡(∃K.M=N+K')| . (DEFAX LESSP (TM& . |∀N M.N<M≡(∃K.M=N+K')|)) . ((LESSP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . <)) . ORDERING#4 . NIL . DEFINED .)) M N K J I ADD1 PLUS) . NIL . (ORDERING#4) . NIL . ORDERING . NIL . 4 .)(|∀N K.0*N=0∧N'*K=N*K+K| . (DEFAX TIMES (TM& . |∀N K.0*N=0∧N'*K=N*K+K|)) . ((TIMES . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 935) (INFIX& . *)) . MULTIP#2 . NIL . DEFINED .)) M N K J I ADD1 PLUS) . NIL . (MULTIP#2) . NIL . MULTIP . NIL . 2 .)(|∀DF NILCASE DEF.(∃FUN.(∀PARS X U.FUN(NIL,PARS)=NILCASE(PARS)∧ FUN(X.U,PARS)= DEF(X,U,FUN(U,DF(X,PARS)),PARS)))| . (AXIOM (TM& . |∀DF NILCASE DEF.(∃FUN.(∀PARS X U.FUN(NIL,PARS)=NILCASE(PARS)∧ FUN(X.U,PARS)= DEF(X,U,FUN(U,DF(X,PARS)),PARS)))|)) . (LISTP SEXP W V U Z Y X CONS PARS DF2 DF1 DF NILCASE (FUN . (|(GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#34 . NIL . VARIABLE .)) (DEF . (|(GROUND⊗GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#34 . NIL . VARIABLE .))) . NIL . (LISPAX#34) . NIL . LISPAX . NIL . 34 .)(|∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X.Y))⊃(∀X.PHI(X))| . (AXIOM (TM& . |∀PHI.(∀X.ATOM X⊃PHI(X))∧(∀X Y.PHI(X)∧PHI(Y)⊃PHI(X.Y))⊃(∀X.PHI(X))|)) . (ATOM SEXP Z Y X PHI CONS) . NIL . (LISPAX#35) . NIL . LISPAX . NIL . 35 .)(|∀N M.M<N∨M=N∨M>N| . (AXIOM (TM& . |∀N M.M<N∨M=N∨M>N|)) . (M N K J I ADD1 PLUS LESSP GREATERP) . NIL . (ORDERING#5) . NIL . ORDERING . NIL . 5 .)(|∀N M.M=N⊃¬M<N∧¬M>N| . (AXIOM (TM& . |∀N M.M=N⊃¬M<N∧¬M>N|)) . (M N K J I ADD1 PLUS LESSP GREATERP) . NIL . (ORDERING#6) . NIL . ORDERING . NIL . 6 .)(|∀N M.M>N⊃¬M=N∧¬M<N| . (AXIOM (TM& . |∀N M.M>N⊃¬M=N∧¬M<N|)) . (M N K J I ADD1 PLUS LESSP GREATERP) . NIL . (ORDERING#7) . NIL . ORDERING . NIL . 7 .)(|∀N M.M<N⊃¬M=N∧¬M>N| . (AXIOM (TM& . |∀N M.M<N⊃¬M=N∧¬M>N|)) . (M N K J I ADD1 PLUS LESSP GREATERP) . NIL . (ORDERING#8) . NIL . ORDERING . NIL . 8 .)(|∀N M.M>N≡N<M| . (AXIOM (TM& . |∀N M.M>N≡N<M|)) . (M N K J I ADD1 PLUS LESSP GREATERP) . NIL . (ORDERING#9) . NIL . ORDERING . NIL . 9 .)(NIL . (DECL GRTEQP (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT) (INFIXNAME: ≥) (BINDINGPOWER: 920)) . ((GRTEQP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . ≥)) . ORDERING#10 . NIL . CONSTANT .))) . NIL . NIL . NIL . ORDERING . NIL . 10 .)(NIL . (DECL LSSEQP (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT) (INFIXNAME: ≤) (BINDINGPOWER: 920)) . ((LSSEQP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . ≤)) . ORDERING#11 . NIL . CONSTANT .))) . NIL . NIL . NIL . ORDERING . NIL . 11 .)(|∀N M.M≥N≡M>N∨M=N| . (DEFAX GRTEQP (TM& . |∀N M.M≥N≡M>N∨M=N|)) . ((GRTEQP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . ≥)) . ORDERING#12 . NIL . DEFINED .)) M N K J I ADD1 PLUS GREATERP) . NIL . (ORDERING#12) . NIL . ORDERING . NIL . 12 .)(|∀N M.M≤N≡M<N∨M=N| . (DEFAX LSSEQP (TM& . |∀N M.M≤N≡M<N∨M=N|)) . ((LSSEQP . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 920) (INFIX& . ≤)) . ORDERING#13 . NIL . DEFINED .)) M N K J I ADD1 PLUS LESSP) . NIL . (ORDERING#13) . NIL . ORDERING . NIL . 13 .)(|∀N M.NATNUM(N*M)| . (AXIOM (TM& . |∀N M.NATNUM(N*M)|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#3) . NIL . MULTIP . NIL . 3 .)(|∀N.N*0=0∧1*N=N∧N*1=N| . (AXIOM (TM& . |∀N.N*0=0∧1*N=N∧N*1=N|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#4) . NIL . MULTIP . NIL . 4 .)(|∀K N.N*K'=N*K+N| . (AXIOM (TM& . |∀K N.N*K'=N*K+N|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#5) . NIL . MULTIP . NIL . 5 .)(|∀N K M.¬K=0⊃K*M=K*N≡M=N| . (AXIOM (TM& . |∀N K M.¬K=0⊃K*M=K*N≡M=N|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#6) . NIL . MULTIP . NIL . 6 .)(|∀N K M.¬K=0⊃M*K=N*K≡M=N| . (AXIOM (TM& . |∀N K M.¬K=0⊃M*K=N*K≡M=N|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#7) . NIL . MULTIP . NIL . 7 .)(|∀N M.N*M=M*N| . (AXIOM (TM& . |∀N M.N*M=M*N|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#8) . NIL . MULTIP . NIL . 8 .)(|∀N K.¬N=0⊃N*K=0≡K=0| . (AXIOM (TM& . |∀N K.¬N=0⊃N*K=0≡K=0|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#9) . NIL . MULTIP . NIL . 9 .)(|∀N K.¬N=0⊃K*N=0≡K=0| . (AXIOM (TM& . |∀N K.¬N=0⊃K*N=0≡K=0|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#10) . NIL . MULTIP . NIL . 10 .)(|∀A N.(∀M.M<N⊃A(M))≡ALL(N,A)| . (AXIOM (TM& . |∀A N.(∀M.M<N⊃A(M))≡ALL(N,A)|)) . (M N K J I SET C B A ADD1 PLUS LESSP ALL) . NIL . (ALL#5) . NIL . ALL . NIL . 5 .)(|∀A N.(∃M.M<N∧A(M))≡SOME(N,A)| . (AXIOM (TM& . |∀A N.(∃M.M<N∧A(M))≡SOME(N,A)|)) . (M N K J I SET C B A ADD1 PLUS LESSP SOME) . NIL . (ALL#6) . NIL . ALL . NIL . 6 .)(|∀ATOMCASE DEFSEXP DF1 DF2.(∃FUN.(∀PARS X Y Z.(ATOM Z⊃ FUN(Z,PARS)=ATOMCASE(Z,PARS))∧ FUN(X.Y,PARS)= DEFSEXP(X,Y,FUN(X,DF1(X,Y,PARS)), FUN(Y,DF2(X,Y,PARS)), PARS)))| . (AXIOM (TM& . |∀ATOMCASE DEFSEXP DF1 DF2.(∃FUN.(∀PARS X Y Z.(ATOM Z⊃ FUN(Z,PARS)=ATOMCASE(Z,PARS))∧ FUN(X.Y,PARS)= DEFSEXP(X,Y,FUN(X,DF1(X,Y,PARS)), FUN(Y,DF2(X,Y,PARS)), PARS)))|)) . (ATOM LISTP SEXP W V U Z Y X CONS PARS DF2 DF1 DF NILCASE FUN DEF (DEFSEXP . (|(GROUND⊗GROUND⊗GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#36 . NIL . VARIABLE .)) (ATOMCASE . (|(GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#36 . NIL . VARIABLE .))) . NIL . (LISPAX#36) . NIL . LISPAX . NIL . 36 .)(NIL . (DECL (ARB ARB1 ARB2) (TYPE: (TY& . ?ARBITRARY))) . ((ARB2 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#37 . NIL . VARIABLE .)) (ARB1 . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#37 . NIL . VARIABLE .)) (ARB . (?ARBITRARY . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#37 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 37 .)(|∀N M.M≥N≡N≤M| . (AXIOM (TM& . |∀N M.M≥N≡N≤M|)) . (M N K J I ADD1 PLUS LESSP GREATERP GRTEQP LSSEQP) . NIL . (ORDERING#14) . NIL . ORDERING . NIL . 14 .)(|∀N M K.N<M∧M<K⊃N<K| . (AXIOM (TM& . |∀N M K.N<M∧M<K⊃N<K|)) . (M N K J I ADD1 PLUS LESSP) . NIL . (ORDERING#15) . NIL . ORDERING . NIL . 15 .)(|∀N M K.K>M∧M>N⊃K>N| . (AXIOM (TM& . |∀N M K.K>M∧M>N⊃K>N|)) . (M N K J I ADD1 PLUS GREATERP) . NIL . (ORDERING#16) . NIL . ORDERING . NIL . 16 .)(|∀N M K.N≤M∧M<K⊃N<K| . (AXIOM (TM& . |∀N M K.N≤M∧M<K⊃N<K|)) . (M N K J I ADD1 PLUS LESSP LSSEQP) . NIL . (ORDERING#17) . NIL . ORDERING . NIL . 17 .)(|∀N M K.N<M∧M≤K⊃N<K| . (AXIOM (TM& . |∀N M K.N<M∧M≤K⊃N<K|)) . (M N K J I ADD1 PLUS LESSP LSSEQP) . NIL . (ORDERING#18) . NIL . ORDERING . NIL . 18 .)(|∀N M K.N≤M∧M≤K⊃N≤K| . (AXIOM (TM& . |∀N M K.N≤M∧M≤K⊃N≤K|)) . (M N K J I ADD1 PLUS LESSP LSSEQP) . NIL . (ORDERING#19) . NIL . ORDERING . NIL . 19 .)(|∀N M.N+M'>N| . (AXIOM (TM& . |∀N M.N+M'>N|)) . (M N K J I ADD1 PLUS GREATERP) . NIL . (ORDERING#20) . NIL . ORDERING . NIL . 20 .)(|∀N M.N'<M'≡N<M| . (AXIOM (TM& . |∀N M.N'<M'≡N<M|)) . (M N K J I ADD1 PLUS LESSP) . NIL . (ORDERING#21) . NIL . ORDERING . NIL . 21 .)(|∀N M K.M+K>N+K≡M>N| . (AXIOM (TM& . |∀N M K.M+K>N+K≡M>N|)) . (M N K J I ADD1 PLUS GREATERP) . NIL . (ORDERING#22) . NIL . ORDERING . NIL . 22 .)(|∀N M K.M+K<N+K≡M<N| . (AXIOM (TM& . |∀N M K.M+K<N+K≡M<N|)) . (M N K J I ADD1 PLUS LESSP) . NIL . (ORDERING#23) . NIL . ORDERING . NIL . 23 .)(|∀N M I J.N>M∧I>J⊃N+I>M+J| . (AXIOM (TM& . |∀N M I J.N>M∧I>J⊃N+I>M+J|)) . (M N K J I ADD1 PLUS GREATERP) . NIL . (ORDERING#24) . NIL . ORDERING . NIL . 24 .)(|∀N M I J.N≥M∧I>J⊃N+I>M+J| . (AXIOM (TM& . |∀N M I J.N≥M∧I>J⊃N+I>M+J|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP) . NIL . (ORDERING#25) . NIL . ORDERING . NIL . 25 .)(|∀N M I J.N>M∧I≥J⊃N+I>M+J| . (AXIOM (TM& . |∀N M I J.N>M∧I≥J⊃N+I>M+J|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP) . NIL . (ORDERING#26) . NIL . ORDERING . NIL . 26 .)(|∀N M I J.N≥M∧I≥J⊃N+I≥M+J| . (AXIOM (TM& . |∀N M I J.N≥M∧I≥J⊃N+I≥M+J|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP) . NIL . (ORDERING#27) . NIL . ORDERING . NIL . 27 .)(|∀N.N≥0| . (AXIOM (TM& . |∀N.N≥0|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP) . NIL . (ORDERING#28) . NIL . ORDERING . NIL . 28 .)(|∀N.¬N<0| . (AXIOM (TM& . |∀N.¬N<0|)) . (M N K J I ADD1 PLUS LESSP) . NIL . (ORDERING#29) . NIL . ORDERING . NIL . 29 .)(|∀N.¬N=0⊃0<N| . (AXIOM (TM& . |∀N.¬N=0⊃0<N|)) . (M N K J I ADD1 PLUS LESSP) . NIL . (ORDERING#30) . NIL . ORDERING . NIL . 30 .)(|∀N.N'≥1| . (AXIOM (TM& . |∀N.N'≥1|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP) . NIL . (ORDERING#31) . NIL . ORDERING . NIL . 31 .)(|∀N M.N>M⊃N≥M'| . (AXIOM (TM& . |∀N M.N>M⊃N≥M'|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP) . NIL . (ORDERING#32) . NIL . ORDERING . NIL . 32 .)(|∀M N.M<N'⊃M≤N| . (AXIOM (TM& . |∀M N.M<N'⊃M≤N|)) . (M N K J I ADD1 PLUS LESSP LSSEQP) . NIL . (ORDERING#33) . NIL . ORDERING . NIL . 33 .)(|∀A.(∃M.A(M))⊃(∃N.A(N)∧(∀M.A(M)⊃N<M))| . (AXIOM (TM& . |∀A.(∃M.A(M))⊃(∃N.A(N)∧(∀M.A(M)⊃N<M))|)) . (M N K J I SET C B A ADD1 PLUS LESSP) . NIL . (ORDERING#34) . NIL . ORDERING . NIL . 34 .)(NIL . (DECL BIGFUN (TYPE: (TY& . |(GROUND⊗GROUND⊗(@ARB)⊗(@ARB))→(@ARB)|))) . ((BIGFUN . (|(GROUND⊗GROUND⊗(@ARB)⊗(@ARB))→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#38 . NIL . VARIABLE .)) (ARB . LISPAX#37)) . NIL . NIL . NIL . LISPAX . NIL . 38 .)(NIL . (DECL (DEFINED_FUN ATOM_FUN) (TYPE: (TY& . |GROUND→(@ARB)|))) . ((ATOM_FUN . (|GROUND→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#39 . NIL . VARIABLE .)) (DEFINED_FUN . (|GROUND→(@ARB)| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#39 . NIL . VARIABLE .)) (ARB . LISPAX#37)) . NIL . NIL . NIL . LISPAX . NIL . 39 .)(¬N=0∧¬M=0⊃¬N*M=0 . (DERIVE (TM& . ¬N=0∧¬M=0⊃¬N*M=0) ((LR& MULTIP#10)) NIL) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#10 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4) . NIL . MULTIP . NIL . 11 .)(|∀N K M.N*(K+M)=N*K+N*M| . (AXIOM (TM& . |∀N K M.N*(K+M)=N*K+N*M|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#12) . NIL . MULTIP . NIL . 12 .)(|∀N M K.(M+K)*N=M*N+K*N| . (AXIOM (TM& . |∀N M K.(M+K)*N=M*N+K*N|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#13) . NIL . MULTIP . NIL . 13 .)(|∀N M K.N>M∧¬K=0⊃N*K>M*K| . (AXIOM (TM& . |∀N M K.N>M∧¬K=0⊃N*K>M*K|)) . (M N K J I ADD1 PLUS GREATERP TIMES) . NIL . (MULTIP#14) . NIL . MULTIP . NIL . 14 .)(|∀N M K.N<M∧¬K=0⊃N*K<M*K| . (AXIOM (TM& . |∀N M K.N<M∧¬K=0⊃N*K<M*K|)) . (M N K J I ADD1 PLUS LESSP TIMES) . NIL . (MULTIP#15) . NIL . MULTIP . NIL . 15 .)(|∀N M K.¬K=0∧M*K>N*K⊃M>N| . (AXIOM (TM& . |∀N M K.¬K=0∧M*K>N*K⊃M>N|)) . (M N K J I ADD1 PLUS GREATERP TIMES) . NIL . (MULTIP#16) . NIL . MULTIP . NIL . 16 .)(|∀N M K.¬K=0∧M*K=N*K⊃M=N| . (AXIOM (TM& . |∀N M K.¬K=0∧M*K=N*K⊃M=N|)) . (M N K J I ADD1 PLUS TIMES) . NIL . (MULTIP#17) . NIL . MULTIP . NIL . 17 .)(|∀N M K.¬K=0∧M*K<N*K⊃M<N| . (AXIOM (TM& . |∀N M K.¬K=0∧M*K<N*K⊃M<N|)) . (M N K J I ADD1 PLUS LESSP TIMES) . NIL . (MULTIP#18) . NIL . MULTIP . NIL . 18 .)(|∀N M I J.N>M∧I>J⊃N*I>M*J| . (AXIOM (TM& . |∀N M I J.N>M∧I>J⊃N*I>M*J|)) . (M N K J I ADD1 PLUS GREATERP TIMES) . NIL . (MULTIP#19) . NIL . MULTIP . NIL . 19 .)(|∀N M I J.¬M=0∧N≥M∧I>J⊃N*I>M*J| . (AXIOM (TM& . |∀N M I J.¬M=0∧N≥M∧I>J⊃N*I>M*J|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP TIMES) . NIL . (MULTIP#20) . NIL . MULTIP . NIL . 20 .)(|∀N M I J.¬J=0∧N>M∧I≥J⊃N*I>M*J| . (AXIOM (TM& . |∀N M I J.¬J=0∧N>M∧I≥J⊃N*I>M*J|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP TIMES) . NIL . (MULTIP#21) . NIL . MULTIP . NIL . 21 .)(|∀N M I J.N≥M∧I≥J⊃N*I≥M*J| . (AXIOM (TM& . |∀N M I J.N≥M∧I≥J⊃N*I≥M*J|)) . (M N K J I ADD1 PLUS GREATERP GRTEQP TIMES) . NIL . (MULTIP#22) . NIL . MULTIP . NIL . 22 .)(|∀BIGFUN ATOM_FUN.(∃DEFINED_FUN.(∀X Y.(ATOM X⊃DEFINED_FUN(X)=ATOM_FUN(X))∧ DEFINED_FUN(X.Y)= BIGFUN(X,Y,DEFINED_FUN(X), DEFINED_FUN(Y))))| . (AXIOM (TM& . |∀BIGFUN ATOM_FUN.(∃DEFINED_FUN.(∀X Y.(ATOM X⊃DEFINED_FUN(X)=ATOM_FUN(X))∧ DEFINED_FUN(X.Y)= BIGFUN(X,Y,DEFINED_FUN(X), DEFINED_FUN(Y))))|)) . (ATOM SEXP Z Y X CONS (ARB . LISPAX#37) BIGFUN ATOM_FUN DEFINED_FUN) . NIL . (LISPAX#40) . NIL . LISPAX . NIL . 40 .)(NIL . (DECL LIST (TYPE: (TY& . |(GROUND*)→GROUND|)) (SYNTYPE: CONSTANT)) . ((LIST . (|(GROUND*)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#41 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 41 .)(NIL . (DECL LST (TYPE: (TY& . GROUND*))) . ((LST . (GROUND* . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#42 . NIL . VARIABLE .))) . NIL . NIL . NIL . LISPAX . NIL . 42 .)(|LIST(())=NIL| . (AXIOM (TM& . |LIST(())=NIL|)) . (LIST) . NIL . (LISPAX#43) . NIL . LISPAX . NIL . 43 .)(|∀LST.LISTP LIST(LST)| . (AXIOM (TM& . |∀LST.LISTP LIST(LST)|)) . (LISTP LIST LST) . NIL . (LISPAX#44) . NIL . LISPAX . NIL . 44 .)(|∀X LST.LIST(X,LST)=X.LIST(LST)| . (AXIOM (TM& . |∀X LST.LIST(X,LST)=X.LIST(LST)|)) . (SEXP Z Y X CONS LIST LST) . NIL . (LISPAX#45) . NIL . LISPAX . NIL . 45 .)(NIL . (DECL APPEND (TYPE: (TY& . |(GROUND⊗GROUND⊗(GROUND*))→GROUND|)) (SYNTYPE: CONSTANT) (ASSOCIATIVITY: BOTH) (INFIXNAME: **) (BINDINGPOWER: 840)) . ((APPEND . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 840) (INFIX& . **)) . LISPAX#46 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 46 .)(|∀X U V.NIL ** V=V∧X.U ** V=X.(U ** V)| . (DEFAX APPEND (TM& . |∀X U V.NIL ** V=V∧X.U ** V=X.(U ** V)|)) . ((APPEND . (|(GROUND⊗GROUND⊗(GROUND*))→GROUND| . (SYMBOL& UNIVERSAL NIL) . BOTH . ((BINDP& . 840) (INFIX& . **)) . LISPAX#47 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#47) . NIL . LISPAX . NIL . 47 .)(|∀U V.LISTP U ** V| . (AXIOM (TM& . |∀U V.LISTP U ** V|)) . (LISTP SEXP W V U Z Y X CONS APPEND) . NIL . (LISPAX#48) . NIL . LISPAX . NIL . 48 .)(|∀U.U ** NIL=U| . (AXIOM (TM& . |∀U.U ** NIL=U|)) . (LISTP SEXP W V U Z Y X CONS APPEND) . NIL . (LISPAX#49) . NIL . LISPAX . NIL . 49 .)(|∀X V.X.NIL ** V=X.V| . (AXIOM (TM& . |∀X V.X.NIL ** V=X.V|)) . (LISTP SEXP W V U Z Y X CONS APPEND) . NIL . (LISPAX#50) . NIL . LISPAX . NIL . 50 .)(NIL . (DECL (ALLP SOMEP) (SYNTYPE: CONSTANT) (TYPE: (TY& . |((@PHI)⊗GROUND)→TRUTHVAL|))) . ((SOMEP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#51 . NIL . CONSTANT .)) (ALLP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#51 . NIL . CONSTANT .)) PHI) . NIL . NIL . NIL . LISPAX . NIL . 51 .)(|∀PHI X U.ALLP(PHI,NIL)∧ALLP(PHI,X.U)=(IF PHI(X) THEN ALLP(PHI,U) ELSE FALSE)| . (DEFAX ALLP (TM& . |∀PHI X U.ALLP(PHI,NIL)∧ALLP(PHI,X.U)=(IF PHI(X) THEN ALLP(PHI,U) ELSE FALSE)|)) . ((ALLP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#52 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X PHI CONS (SOMEP . LISPAX#51)) . NIL . (LISPAX#52) . NIL . LISPAX . NIL . 52 .)(|∀PHI X U.¬SOMEP(PHI,NIL)∧ SOMEP(PHI,X.U)=(IF PHI(X) THEN TRUE ELSE SOMEP(PHI,U))| . (DEFAX SOMEP (TM& . |∀PHI X U.¬SOMEP(PHI,NIL)∧ SOMEP(PHI,X.U)=(IF PHI(X) THEN TRUE ELSE SOMEP(PHI,U))|)) . ((SOMEP . (|((@PHI)⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#53 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X PHI CONS) . NIL . (LISPAX#53) . NIL . LISPAX . NIL . 53 .)(|∀FN X U.MAPCAR(FN,NIL)=NIL∧MAPCAR(FN,X.U)=FN(X).MAPCAR(FN,U)| . (DEFAX MAPCAR (TM& . |∀FN X U.MAPCAR(FN,NIL)=NIL∧MAPCAR(FN,X.U)=FN(X).MAPCAR(FN,U)|)) . ((MAPCAR . (|((GROUND→GROUND)⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#54 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS (FN . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#54 . NIL . VARIABLE .))) . NIL . (LISPAX#54) . NIL . LISPAX . NIL . 54 .)(NIL . (DECL (ALIST) (TYPE: (TY& . GROUND)) (SORT: (TM& . ALISTP))) . ((ALIST . (GROUND . (SYMBOL& ALISTP NIL) . NIL . NIL . LISPAX#55 . NIL . VARIABLE .)) ALISTP) . NIL . NIL . NIL . LISPAX . NIL . 55 .)(|∀ALIST.LISTP ALIST| . (AXIOM (TM& . |∀ALIST.LISTP ALIST|)) . (LISTP ALISTP ALIST) . NIL . (LISPAX#56) . NIL . LISPAX . NIL . 56 .)(|∀U.ALISTP U≡(¬NULL U⊃¬ATOM CAR U∧ATOM CAR (CAR U)∧ALISTP CDR U)| . (AXIOM (TM& . |∀U.ALISTP U≡(¬NULL U⊃¬ATOM CAR U∧ATOM CAR (CAR U)∧ALISTP CDR U)|)) . (CAR CDR ATOM NULL LISTP ALISTP W V U) . NIL . (LISPAX#57) . NIL . LISPAX . NIL . 57 .)(|∀XA Y ALIST.ALISTP NIL∧ALISTP (XA.Y).ALIST| . (AXIOM (TM& . |∀XA Y ALIST.ALISTP NIL∧ALISTP (XA.Y).ALIST|)) . (ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST) . NIL . (LISPAX#58) . NIL . LISPAX . NIL . 58 .)(NIL . (DECL ASSOC (TYPE: (TY& . |(GROUND⊗GROUND)→GROUND|)) (SYNTYPE: CONSTANT)) . ((ASSOC . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#59 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 59 .)(|∀X XA Y ALIST.ASSOC(X,NIL)=NIL∧ ASSOC(X,(XA.Y).ALIST)=(IF X=XA THEN XA.Y ELSE ASSOC(X,ALIST))| . (DEFAX ASSOC (TM& . |∀X XA Y ALIST.ASSOC(X,NIL)=NIL∧ ASSOC(X,(XA.Y).ALIST)=(IF X=XA THEN XA.Y ELSE ASSOC(X,ALIST))|)) . ((ASSOC . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#60 . NIL . DEFINED .)) ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST) . NIL . (LISPAX#60) . NIL . LISPAX . NIL . 60 .)(|∀X ALIST.SEXP ASSOC(X,ALIST)| . (AXIOM (TM& . |∀X ALIST.SEXP ASSOC(X,ALIST)|)) . (ATOM ALISTP SEXP Z Y X ZA YA XA CONS ALIST ASSOC) . NIL . (LISPAX#61) . NIL . LISPAX . NIL . 61 .)(NIL . (DECL MEMBER (TYPE: (TY& . |(GROUND⊗GROUND)→TRUTHVAL|)) (SYNTYPE: CONSTANT)) . ((MEMBER . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#62 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 62 .)(|∀X Y U.¬MEMBER(X,NIL)∧MEMBER(X,Y.U)=(X=Y∨MEMBER(X,U))| . (DEFAX MEMBER (TM& . |∀X Y U.¬MEMBER(X,NIL)∧MEMBER(X,Y.U)=(X=Y∨MEMBER(X,U))|)) . ((MEMBER . (|(GROUND⊗GROUND)→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#63 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS) . NIL . (LISPAX#63) . NIL . LISPAX . NIL . 63 .)(NIL . (DECL UNIQUENESS (TYPE: (TY& . GROUND→TRUTHVAL)) (SYNTYPE: CONSTANT)) . ((UNIQUENESS . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#64 . NIL . CONSTANT .))) . NIL . NIL . NIL . LISPAX . NIL . 64 .)(|∀U X.UNIQUENESS(NIL)∧(UNIQUENESS(X.U)≡¬MEMBER(X,U)∧UNIQUENESS(U))| . (DEFAX UNIQUENESS (TM& . |∀U X.UNIQUENESS(NIL)∧(UNIQUENESS(X.U)≡¬MEMBER(X,U)∧UNIQUENESS(U))|)) . ((UNIQUENESS . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#65 . NIL . DEFINED .)) LISTP SEXP W V U Z Y X CONS MEMBER) . NIL . (LISPAX#65) . NIL . LISPAX . NIL . 65 .)(|∀U.SEXP CAR U| . (UE (UELST& (PHI . |λU.SEXP CAR U|)) (LN& . LISPAX#30) NIL) . (CAR LISTP SEXP W V U Z Y X PHI CONS) . NIL . (LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61) . NIL . LISPAX . NIL . 66 .)(|∀U.LISTP CDR U| . (UE (UELST& (PHI . |λU.LISTP CDR U|)) (LN& . LISPAX#30) NIL) . (CDR LISTP SEXP W V U Z Y X PHI CONS) . NIL . (LISPAX#30 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66) . NIL . LISPAX . NIL . 67 .)(|CADR=(λXV.CAR (CDR XV))| . (DEFINE CADR (TM& . |CADR=(λXV.CAR (CDR XV))|) NIL) . (CAR CDR SEXP (XV . (GROUND . (SYMBOL& SEXP NIL) . NIL . ((BINDP& . 1000)) . LISPAX#68 . NIL . VARIABLE .)) (CADR . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#68 . NIL . DEFINED .))) . NIL . (LISPAX#68 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67) . NIL . LISPAX . NIL . 68 .)(|CDDR=(λXV.CDR (CDR XV))| . (DEFINE CDDR (TM& . |CDDR=(λXV.CDR (CDR XV))|) NIL) . (CAR CDR SEXP XV CADR (CDDR . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . LISPAX#69 . NIL . DEFINED .))) . NIL . (LISPAX#69 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67) . NIL . LISPAX . NIL . 69 .)(|∀U.SEXP CAR U| . (AXIOM (TM& . |∀U.SEXP CAR U|)) . (CAR LISTP SEXP W V U) . NIL . (LISPAX#70) . NIL . LISPAX . NIL . 70 .)(|∀U.LISTP CDR U| . (AXIOM (TM& . |∀U.LISTP CDR U|)) . (CDR LISTP W V U) . NIL . (LISPAX#71) . NIL . LISPAX . NIL . 71 .)(|∀U.¬NULL CADR(U)∧NULL CDDR(U)⊃LIST(CAR U,CADR(U))=U| . (AXIOM (TM& . |∀U.¬NULL CADR(U)∧NULL CDDR(U)⊃LIST(CAR U,CADR(U))=U|)) . (CAR CDR NULL LISTP SEXP W V U LIST XV CADR CDDR) . NIL . (LISPAX#72) . NIL . LISPAX . NIL . 72 .)(|∀N.¬NULL N| . (AXIOM (TM& . |∀N.¬NULL N|)) . (M N K J I NULL) . NIL . (LISPAX#73) . NIL . LISPAX . NIL . 73 .)(|∀N.SEXP N| . (AXIOM (TM& . |∀N.SEXP N|)) . (M N K J I SEXP) . NIL . (LISPAX#74) . NIL . LISPAX . NIL . 74 .)(|∀X Y.CAR LIST(X,Y)=X| . (AXIOM (TM& . |∀X Y.CAR LIST(X,Y)=X|)) . (CAR SEXP Z Y X LIST) . NIL . (LISPAX#75) . NIL . LISPAX . NIL . 75 .)(|∀X Y.CADR(LIST(X,Y))=Y| . (AXIOM (TM& . |∀X Y.CADR(LIST(X,Y))=Y|)) . (CAR CDR SEXP Z Y X LIST XV CADR) . NIL . (LISPAX#76) . NIL . LISPAX . NIL . 76 .)(|∀Q.NULL CDDR(Q)| . (AXIOM (TM& . |∀Q.NULL CDDR(Q)|)) . (CAR CDR NULL SEXP XV CADR CDDR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q) . NIL . (FRACTIONS#3) . NIL . FRACTIONS . NIL . 3 .)(|∀M N.¬N=0⊃FR(LIST(M,N))| . (AXIOM (TM& . |∀M N.¬N=0⊃FR(LIST(M,N))|)) . (M N K J I LIST FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q) . NIL . (FRACTIONS#4) . NIL . FRACTIONS . NIL . 4 .)(|∀Q.NATNUM(CAR Q)∧NATNUM(CADR(Q))∧¬CADR(Q)=0| . (AXIOM (TM& . |∀Q.NATNUM(CAR Q)∧NATNUM(CADR(Q))∧¬CADR(Q)=0|)) . (CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q) . NIL . (FRACTIONS#5) . NIL . FRACTIONS . NIL . 5 .)(|∀Q.LIST(CAR Q,CADR(Q))=Q| . (AXIOM (TM& . |∀Q.LIST(CAR Q,CADR(Q))=Q|)) . (CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q) . NIL . (FRACTIONS#6) . NIL . FRACTIONS . NIL . 6 .)(NIL . (DECL EF (TYPE: (TY& . |((@Q)⊗(@Q))→TRUTHVAL|))) . ((EF . (|((@Q)⊗(@Q))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRACTIONS#7 . NIL . VARIABLE .)) Q) . NIL . NIL . NIL . FRACTIONS . NIL . 7 .)(|EF=(λQ Q0.(IF CAR Q*CADR(Q0)=CADR(Q)*CAR Q0 THEN TRUE ELSE FALSE))| . (DEFINE EF (TM& . |EF=(λQ Q0.(IF CAR Q*CADR(Q0)=CADR(Q)*CAR Q0 THEN TRUE ELSE FALSE))|) NIL) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q (EF . (|((@Q)⊗(@Q))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRACTIONS#8 . NIL . DEFINED .))) . NIL . (FRACTIONS#8 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6) . NIL . FRACTIONS . NIL . 8 .)(|∀Q.FR(LIST(CAR Q,CADR(Q)))| . (AXIOM (TM& . |∀Q.FR(LIST(CAR Q,CADR(Q)))|)) . (CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q) . NIL . (FRACTIONS#9) . NIL . FRACTIONS . NIL . 9 .)(|∀Q.EF(Q,Q)| . (AXIOM (TM& . |∀Q.EF(Q,Q)|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF) . NIL . (FRACTIONS#10) . NIL . FRACTIONS . NIL . 10 .)(|∀Q Q0.EF(Q,Q0)⊃EF(Q0,Q)| . (AXIOM (TM& . |∀Q Q0.EF(Q,Q0)⊃EF(Q0,Q)|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF) . NIL . (FRACTIONS#11) . NIL . FRACTIONS . NIL . 11 .)(|∀Q Q1 Q2.EF(Q,Q1)∧EF(Q1,Q2)⊃EF(Q,Q2)| . (AXIOM (TM& . |∀Q Q1 Q2.EF(Q,Q1)∧EF(Q1,Q2)⊃EF(Q,Q2)|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF) . NIL . (FRACTIONS#12) . NIL . FRACTIONS . NIL . 12 .)(|∀Q Q1 Q2 Q3.EF(Q,Q1)∧EF(Q1,Q2)∧EF(Q2,Q3)⊃EF(Q,Q3)| . (AXIOM (TM& . |∀Q Q1 Q2 Q3.EF(Q,Q1)∧EF(Q1,Q2)∧EF(Q2,Q3)⊃EF(Q,Q3)|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF) . NIL . (FRACTIONS#13) . NIL . FRACTIONS . NIL . 13 .)(|∀Q N.¬N=0⊃EF(LIST(CAR Q*N,CADR(Q)*N),Q)| . (AXIOM (TM& . |∀Q N.¬N=0⊃EF(LIST(CAR Q*N,CADR(Q)*N),Q)|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF) . NIL . (FRACTIONS#14) . NIL . FRACTIONS . NIL . 14 .)(|GF=(λQ Q0.(IF CAR Q*CADR(Q0)>CADR(Q)*CAR Q0 THEN TRUE ELSE FALSE))| . (DEFINE GF (TM& . |GF=(λQ Q0.(IF CAR Q*CADR(Q0)>CADR(Q)*CAR Q0 THEN TRUE ELSE FALSE))|) NIL) . (M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q (GF . (|((@Q)⊗(@Q))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRORDERING#2 . NIL . DEFINED .))) . NIL . (FRORDERING#2 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9) . NIL . FRORDERING . NIL . 2 .)(NIL . (DECL LF (TYPE: (TY& . |((@Q)⊗(@Q))→TRUTHVAL|))) . ((LF . (|((@Q)⊗(@Q))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRORDERING#3 . NIL . VARIABLE .)) Q) . NIL . NIL . NIL . FRORDERING . NIL . 3 .)(|LF=(λQ Q0.(IF CAR Q*CADR(Q0)<CADR(Q)*CAR Q0 THEN TRUE ELSE FALSE))| . (DEFINE LF (TM& . |LF=(λQ Q0.(IF CAR Q*CADR(Q0)<CADR(Q)*CAR Q0 THEN TRUE ELSE FALSE))|) NIL) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q (LF . (|((@Q)⊗(@Q))→TRUTHVAL| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRORDERING#4 . NIL . DEFINED .))) . NIL . (FRORDERING#4 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9) . NIL . FRORDERING . NIL . 4 .)(|∀Q Q0.LF(Q,Q0)∨EF(Q,Q0)∨GF(Q,Q0)| . (AXIOM (TM& . |∀Q Q0.LF(Q,Q0)∨EF(Q,Q0)∨GF(Q,Q0)|)) . (M N K J I ADD1 LESSP GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF GF LF) . NIL . (FRORDERING#5) . NIL . FRORDERING . NIL . 5 .)(|∀Q Q0.EF(Q,Q0)⊃¬LF(Q,Q0)∧¬GF(Q,Q0)| . (AXIOM (TM& . |∀Q Q0.EF(Q,Q0)⊃¬LF(Q,Q0)∧¬GF(Q,Q0)|)) . (M N K J I ADD1 LESSP GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF GF LF) . NIL . (FRORDERING#6) . NIL . FRORDERING . NIL . 6 .)(|∀Q Q0.GF(Q,Q0)⊃¬EF(Q,Q0)∧¬LF(Q,Q0)| . (AXIOM (TM& . |∀Q Q0.GF(Q,Q0)⊃¬EF(Q,Q0)∧¬LF(Q,Q0)|)) . (M N K J I ADD1 LESSP GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF GF LF) . NIL . (FRORDERING#7) . NIL . FRORDERING . NIL . 7 .)(|∀Q Q0.LF(Q,Q0)⊃¬EF(Q,Q0)∧¬GF(Q,Q0)| . (AXIOM (TM& . |∀Q Q0.LF(Q,Q0)⊃¬EF(Q,Q0)∧¬GF(Q,Q0)|)) . (M N K J I ADD1 LESSP GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF GF LF) . NIL . (FRORDERING#8) . NIL . FRORDERING . NIL . 8 .)(|∀Q Q0.GF(Q,Q0)≡LF(Q0,Q)| . (AXIOM (TM& . |∀Q Q0.GF(Q,Q0)≡LF(Q0,Q)|)) . (M N K J I ADD1 LESSP GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q GF LF) . NIL . (FRORDERING#9) . NIL . FRORDERING . NIL . 9 .)(|∀Q Q1 Q0.EF(Q,Q1)∧LF(Q,Q0)⊃LF(Q1,Q0)| . (AXIOM (TM& . |∀Q Q1 Q0.EF(Q,Q1)∧LF(Q,Q0)⊃LF(Q1,Q0)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF) . NIL . (FRORDERING#10) . NIL . FRORDERING . NIL . 10 .)(|∀Q Q0 Q01.LF(Q,Q0)∧EF(Q0,Q01)⊃LF(Q,Q01)| . (AXIOM (TM& . |∀Q Q0 Q01.LF(Q,Q0)∧EF(Q0,Q01)⊃LF(Q,Q01)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF) . NIL . (FRORDERING#11) . NIL . FRORDERING . NIL . 11 .)(|∀Q Q1 Q0 Q01.LF(Q,Q0)∧EF(Q,Q1)∧EF(Q0,Q01)⊃LF(Q1,Q01)| . (AXIOM (TM& . |∀Q Q1 Q0 Q01.LF(Q,Q0)∧EF(Q,Q1)∧EF(Q0,Q01)⊃LF(Q1,Q01)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF) . NIL . (FRORDERING#12) . NIL . FRORDERING . NIL . 12 .)(|∀Q Q1 Q0 Q01.GF(Q,Q0)∧EF(Q,Q1)∧EF(Q0,Q01)⊃GF(Q1,Q01)| . (AXIOM (TM& . |∀Q Q1 Q0 Q01.GF(Q,Q0)∧EF(Q,Q1)∧EF(Q0,Q01)⊃GF(Q1,Q01)|)) . (M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF GF) . NIL . (FRORDERING#13) . NIL . FRORDERING . NIL . 13 .)(NIL . (DECL GEF (TYPE: (TY& . @EF))) . ((GEF . (@EF . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRORDERING#14 . NIL . VARIABLE .)) EF) . NIL . NIL . NIL . FRORDERING . NIL . 14 .)(|∀Q Q0.GEF(Q,Q0)≡EF(Q,Q0)∨GF(Q,Q0)| . (DEFINE GEF (TM& . |∀Q Q0.GEF(Q,Q0)≡EF(Q,Q0)∨GF(Q,Q0)|) NIL) . (M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF GF (GEF . (@EF . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRORDERING#15 . NIL . DEFINED .))) . NIL . (FRORDERING#15 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9) . NIL . FRORDERING . NIL . 15 .)(NIL . (DECL LEF (TYPE: (TY& . @EF))) . ((LEF . (@EF . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRORDERING#16 . NIL . VARIABLE .)) EF) . NIL . NIL . NIL . FRORDERING . NIL . 16 .)(|∀Q Q0.LEF(Q,Q0)≡EF(Q,Q0)∨LF(Q,Q0)| . (DEFINE LEF (TM& . |∀Q Q0.LEF(Q,Q0)≡EF(Q,Q0)∨LF(Q,Q0)|) NIL) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF (LEF . (@EF . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRORDERING#17 . NIL . DEFINED .))) . NIL . (FRORDERING#17 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9) . NIL . FRORDERING . NIL . 17 .)(|∀Q Q1 Q0 Q01.GEF(Q,Q0)∧EF(Q,Q1)∧EF(Q0,Q01)⊃GEF(Q1,Q01)| . (AXIOM (TM& . |∀Q Q1 Q0 Q01.GEF(Q,Q0)∧EF(Q,Q1)∧EF(Q0,Q01)⊃GEF(Q1,Q01)|)) . (M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF GF GEF) . NIL . (FRORDERING#18) . NIL . FRORDERING . NIL . 18 .)(|∀Q Q1 Q0 Q01.LEF(Q,Q0)∧EF(Q,Q1)∧EF(Q0,Q01)⊃LEF(Q1,Q01)| . (AXIOM (TM& . |∀Q Q1 Q0 Q01.LEF(Q,Q0)∧EF(Q,Q1)∧EF(Q0,Q01)⊃LEF(Q1,Q01)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF) . NIL . (FRORDERING#19) . NIL . FRORDERING . NIL . 19 .)(|∀Q Q0.GEF(Q,Q0)≡LEF(Q0,Q)| . (AXIOM (TM& . |∀Q Q0.GEF(Q,Q0)≡LEF(Q0,Q)|)) . (M N K J I ADD1 LESSP GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF GF LF GEF LEF) . NIL . (FRORDERING#20) . NIL . FRORDERING . NIL . 20 .)(|∀Q1 Q2 Q3.LF(Q1,Q2)∧LF(Q2,Q3)⊃LF(Q1,Q3)| . (AXIOM (TM& . |∀Q1 Q2 Q3.LF(Q1,Q2)∧LF(Q2,Q3)⊃LF(Q1,Q3)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q LF) . NIL . (FRORDERING#21) . NIL . FRORDERING . NIL . 21 .)(|∀Q Q1 Q2.LEF(Q,Q1)∧LF(Q1,Q2)⊃LF(Q,Q2)| . (AXIOM (TM& . |∀Q Q1 Q2.LEF(Q,Q1)∧LF(Q1,Q2)⊃LF(Q,Q2)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF) . NIL . (FRORDERING#22) . NIL . FRORDERING . NIL . 22 .)(|∀Q Q1 Q2.LF(Q,Q1)∧LEF(Q1,Q2)⊃LF(Q,Q2)| . (AXIOM (TM& . |∀Q Q1 Q2.LF(Q,Q1)∧LEF(Q1,Q2)⊃LF(Q,Q2)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF) . NIL . (FRORDERING#23) . NIL . FRORDERING . NIL . 23 .)(|∀Q Q1 Q2.LEF(Q,Q1)∧LEF(Q1,Q2)⊃LEF(Q,Q2)| . (AXIOM (TM& . |∀Q Q1 Q2.LEF(Q,Q1)∧LEF(Q1,Q2)⊃LEF(Q,Q2)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF) . NIL . (FRORDERING#24) . NIL . FRORDERING . NIL . 24 .)(|∀Q.(∃Q0.GF(Q0,Q))| . (AXIOM (TM& . |∀Q.(∃Q0.GF(Q0,Q))|)) . (M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q GF) . NIL . (FRORDERING#25) . NIL . FRORDERING . NIL . 25 .)(|∀Q.(∃Q0.LF(Q0,Q))| . (AXIOM (TM& . |∀Q.(∃Q0.LF(Q0,Q))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q LF) . NIL . (FRORDERING#26) . NIL . FRORDERING . NIL . 26 .)(|∀Q Q1.(∃Q0.LF(Q,Q1)⊃LF(Q,Q0)∧LF(Q0,Q1))| . (AXIOM (TM& . |∀Q Q1.(∃Q0.LF(Q,Q1)⊃LF(Q,Q0)∧LF(Q0,Q1))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q LF) . NIL . (FRORDERING#27) . NIL . FRORDERING . NIL . 27 .)(|QZ=LIST(0,1)| . (DEFINE QZ (TM& . |QZ=LIST(0,1)|) NIL) . (LIST FR (QZ . (GROUND . (SYMBOL& FR NIL) . NIL . ((BINDP& . 1000)) . FRORDERING#28 . NIL . DEFINED .))) . NIL . (FRORDERING#28 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9) . NIL . FRORDERING . NIL . 28 .)(|FR(QZ)| . (AXIOM (TM& . |FR(QZ)|)) . (LIST FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q QZ) . NIL . (FRORDERING#29) . NIL . FRORDERING . NIL . 29 .)(|QZEROP=(λQ.EF(Q,QZ))| . (DEFINE QZEROP (TM& . |QZEROP=(λQ.EF(Q,QZ))|) NIL) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF QZ (QZEROP . (GROUND→TRUTHVAL . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRORDERING#30 . NIL . DEFINED .))) . NIL . (FRORDERING#30 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29) . NIL . FRORDERING . NIL . 30 .)(|∀Q.LEF(QZ,Q)| . (AXIOM (TM& . |∀Q.LEF(QZ,Q)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF QZ) . NIL . (FRORDERING#31) . NIL . FRORDERING . NIL . 31 .)(|QONE=LIST(1,1)| . (DEFINE QONE (TM& . |QONE=LIST(1,1)|) NIL) . (LIST FR (QONE . (GROUND . (SYMBOL& FR NIL) . NIL . ((BINDP& . 1000)) . FRORDERING#32 . NIL . DEFINED .))) . NIL . (FRORDERING#32 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31) . NIL . FRORDERING . NIL . 32 .)(|FR(QONE)| . (AXIOM (TM& . |FR(QONE)|)) . (LIST FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q QONE) . NIL . (FRORDERING#33) . NIL . FRORDERING . NIL . 33 .)(|PF=(λQ Q0.LIST(CAR Q*CADR(Q0)+CADR(Q)*CAR Q0,CADR(Q)*CADR(Q0)))| . (DEFINE PF (TM& . |PF=(λQ Q0.LIST(CAR Q*CADR(Q0)+CADR(Q)*CAR Q0,CADR(Q)*CADR(Q0)))|) NIL) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q (PF . (|((@Q)⊗(@Q))→(@Q)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 940)) . FRACTSUM#2 . NIL . DEFINED .))) . NIL . (FRACTSUM#2 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33) . NIL . FRACTSUM . NIL . 2 .)(|∀Q Q0.FR(PF(Q,Q0))| . (AXIOM (TM& . |∀Q Q0.FR(PF(Q,Q0))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q PF) . NIL . (FRACTSUM#3) . NIL . FRACTSUM . NIL . 3 .)(|∀Q Q0 Q1 Q01.EF(Q,Q1)∧EF(Q0,Q01)⊃EF(PF(Q,Q0),PF(Q1,Q01))| . (AXIOM (TM& . |∀Q Q0 Q1 Q01.EF(Q,Q1)∧EF(Q0,Q01)⊃EF(PF(Q,Q0),PF(Q1,Q01))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF PF) . NIL . (FRACTSUM#4) . NIL . FRACTSUM . NIL . 4 .)(|∀Q Q0.CADR(Q)=CADR(Q0)⊃EF(PF(Q,Q0),LIST(CAR Q+CAR Q0,CADR(Q)))| . (AXIOM (TM& . |∀Q Q0.CADR(Q)=CADR(Q0)⊃EF(PF(Q,Q0),LIST(CAR Q+CAR Q0,CADR(Q)))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF PF) . NIL . (FRACTSUM#5) . NIL . FRACTSUM . NIL . 5 .)(|∀Q Q0.EF(PF(Q,Q0),PF(Q0,Q))| . (AXIOM (TM& . |∀Q Q0.EF(PF(Q,Q0),PF(Q0,Q))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF PF) . NIL . (FRACTSUM#6) . NIL . FRACTSUM . NIL . 6 .)(|∀Q Q0 Q01.PF(PF(Q,Q0),Q01)=PF(Q,PF(Q0,Q01))| . (AXIOM (TM& . |∀Q Q0 Q01.PF(PF(Q,Q0),Q01)=PF(Q,PF(Q0,Q01))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q PF) . NIL . (FRACTSUM#7) . NIL . FRACTSUM . NIL . 7 .)(|∀Q Q0.¬EF(Q0,QZ)⊃LF(Q,PF(Q,Q0))| . (AXIOM (TM& . |∀Q Q0.¬EF(Q0,QZ)⊃LF(Q,PF(Q,Q0))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF QZ PF) . NIL . (FRACTSUM#8) . NIL . FRACTSUM . NIL . 8 .)(|∀Q Q0 Q01.LF(Q,Q0)⊃LF(PF(Q,Q01),PF(Q0,Q01))| . (AXIOM (TM& . |∀Q Q0 Q01.LF(Q,Q0)⊃LF(PF(Q,Q01),PF(Q0,Q01))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q LF PF) . NIL . (FRACTSUM#9) . NIL . FRACTSUM . NIL . 9 .)(|∀Q Q0 Q01.EF(Q,Q0)⊃EF(PF(Q,Q01),PF(Q0,Q01))| . (AXIOM (TM& . |∀Q Q0 Q01.EF(Q,Q0)⊃EF(PF(Q,Q01),PF(Q0,Q01))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF PF) . NIL . (FRACTSUM#10) . NIL . FRACTSUM . NIL . 10 .)(|∀Q Q0 Q01.GF(Q,Q0)⊃GF(PF(Q,Q01),PF(Q0,Q01))| . (AXIOM (TM& . |∀Q Q0 Q01.GF(Q,Q0)⊃GF(PF(Q,Q01),PF(Q0,Q01))|)) . (M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q GF PF) . NIL . (FRACTSUM#11) . NIL . FRACTSUM . NIL . 11 .)(|∀Q Q0 Q01.GF(PF(Q,Q01),PF(Q0,Q01))⊃GF(Q,Q0)| . (AXIOM (TM& . |∀Q Q0 Q01.GF(PF(Q,Q01),PF(Q0,Q01))⊃GF(Q,Q0)|)) . (M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q GF PF) . NIL . (FRACTSUM#12) . NIL . FRACTSUM . NIL . 12 .)(|∀Q Q0 Q01.EF(PF(Q,Q01),PF(Q0,Q01))⊃EF(Q,Q0)| . (AXIOM (TM& . |∀Q Q0 Q01.EF(PF(Q,Q01),PF(Q0,Q01))⊃EF(Q,Q0)|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF PF) . NIL . (FRACTSUM#13) . NIL . FRACTSUM . NIL . 13 .)(|∀Q Q0 Q01.LF(PF(Q,Q01),PF(Q0,Q01))⊃LF(Q,Q0)| . (AXIOM (TM& . |∀Q Q0 Q01.LF(PF(Q,Q01),PF(Q0,Q01))⊃LF(Q,Q0)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q LF PF) . NIL . (FRACTSUM#14) . NIL . FRACTSUM . NIL . 14 .)(|∀Q Q0 Q1 Q01.GF(Q,Q0)∧GF(Q1,Q01)⊃GF(PF(Q,Q1),PF(Q0,Q01))| . (AXIOM (TM& . |∀Q Q0 Q1 Q01.GF(Q,Q0)∧GF(Q1,Q01)⊃GF(PF(Q,Q1),PF(Q0,Q01))|)) . (M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q GF PF) . NIL . (FRACTSUM#15) . NIL . FRACTSUM . NIL . 15 .)(|∀Q Q0 Q1 Q01.LEF(Q,Q0)∧LF(Q1,Q01)⊃LF(PF(Q,Q1),PF(Q0,Q01))| . (AXIOM (TM& . |∀Q Q0 Q1 Q01.LEF(Q,Q0)∧LF(Q1,Q01)⊃LF(PF(Q,Q1),PF(Q0,Q01))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF PF) . NIL . (FRACTSUM#16) . NIL . FRACTSUM . NIL . 16 .)(|∀Q Q0 Q1 Q01.LF(Q,Q0)∧LEF(Q1,Q01)⊃LF(PF(Q,Q1),PF(Q0,Q01))| . (AXIOM (TM& . |∀Q Q0 Q1 Q01.LF(Q,Q0)∧LEF(Q1,Q01)⊃LF(PF(Q,Q1),PF(Q0,Q01))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF PF) . NIL . (FRACTSUM#17) . NIL . FRACTSUM . NIL . 17 .)(|∀Q Q0 Q1 Q01.LEF(Q,Q0)∧LEF(Q1,Q01)⊃LEF(PF(Q,Q1),PF(Q0,Q01))| . (AXIOM (TM& . |∀Q Q0 Q1 Q01.LEF(Q,Q0)∧LEF(Q1,Q01)⊃LEF(PF(Q,Q1),PF(Q0,Q01))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF PF) . NIL . (FRACTSUM#18) . NIL . FRACTSUM . NIL . 18 .)(|∀Q.EF(PF(Q,QZ),Q)∧EF(PF(QZ,Q),Q)| . (AXIOM (TM& . |∀Q.EF(PF(Q,QZ),Q)∧EF(PF(QZ,Q),Q)|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF QZ PF) . NIL . (FRACTSUM#19) . NIL . FRACTSUM . NIL . 19 .)(|∀Q0 Q.(∃Q1.LF(Q,Q0)⊃EF(PF(Q,Q1),Q0))| . (AXIOM (TM& . |∀Q0 Q.(∃Q1.LF(Q,Q0)⊃EF(PF(Q,Q1),Q0))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF PF) . NIL . (FRACTSUM#20) . NIL . FRACTSUM . NIL . 20 .)(|∀Q0 Q.LF(Q,Q0)⊃EF(PF(Q,MINUS(Q0,Q)),Q0)| . (DEFINE MINUS (TM& . |∀Q0 Q.LF(Q,Q0)⊃EF(PF(Q,MINUS(Q0,Q)),Q0)|) ((USE (LR& FRACTSUM#20)) (USE (LR& SETS#9)))) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF PF (MINUS . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRACTSUM#21 . NIL . DEFINED .))) . NIL . (FRACTSUM#21 MULTIP#10 LISPAX#30 FRACTSUM#20 SETS#9 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19) . NIL . FRACTSUM . NIL . 21 .)(|TF=(λQ Q0.LIST(CAR Q*CAR Q0,CADR(Q)*CADR(Q0)))| . (DEFINE TF (TM& . |TF=(λQ Q0.LIST(CAR Q*CAR Q0,CADR(Q)*CADR(Q0)))|) NIL) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q (TF . (|((@Q)⊗(@Q))→(@Q)| . (SYMBOL& UNIVERSAL NIL) . NIL . ((BINDP& . 935)) . FRACTMULT#2 . NIL . DEFINED .))) . NIL . (FRACTMULT#2 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19) . NIL . FRACTMULT . NIL . 2 .)(|∀Q Q0.FR(TF(Q,Q0))| . (AXIOM (TM& . |∀Q Q0.FR(TF(Q,Q0))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q TF) . NIL . (FRACTMULT#3) . NIL . FRACTMULT . NIL . 3 .)(|∀Q Q0 Q1 Q01.EF(Q,Q1)∧EF(Q0,Q01)⊃EF(TF(Q,Q0),TF(Q1,Q01))| . (AXIOM (TM& . |∀Q Q0 Q1 Q01.EF(Q,Q1)∧EF(Q0,Q01)⊃EF(TF(Q,Q0),TF(Q1,Q01))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF TF) . NIL . (FRACTMULT#4) . NIL . FRACTMULT . NIL . 4 .)(|∀Q Q0.EF(TF(Q,Q0),TF(Q0,Q))| . (AXIOM (TM& . |∀Q Q0.EF(TF(Q,Q0),TF(Q0,Q))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF TF) . NIL . (FRACTMULT#5) . NIL . FRACTMULT . NIL . 5 .)(|∀Q Q0 Q01.TF(TF(Q,Q0),Q01)=TF(Q,TF(Q0,Q01))| . (AXIOM (TM& . |∀Q Q0 Q01.TF(TF(Q,Q0),Q01)=TF(Q,TF(Q0,Q01))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q TF) . NIL . (FRACTMULT#6) . NIL . FRACTMULT . NIL . 6 .)(|∀Q Q0 Q01.TF(Q,PF(Q0,Q01))=PF(TF(Q,Q0),TF(Q,Q01))| . (AXIOM (TM& . |∀Q Q0 Q01.TF(Q,PF(Q0,Q01))=PF(TF(Q,Q0),TF(Q,Q01))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q PF TF) . NIL . (FRACTMULT#7) . NIL . FRACTMULT . NIL . 7 .)(|∀Q Q1 Q0.GF(Q,Q1)⊃GF(TF(Q,Q0),TF(Q1,Q0))| . (AXIOM (TM& . |∀Q Q1 Q0.GF(Q,Q1)⊃GF(TF(Q,Q0),TF(Q1,Q0))|)) . (M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q GF TF) . NIL . (FRACTMULT#8) . NIL . FRACTMULT . NIL . 8 .)(|∀Q Q1 Q0.EF(Q,Q1)⊃EF(TF(Q,Q0),TF(Q1,Q0))| . (AXIOM (TM& . |∀Q Q1 Q0.EF(Q,Q1)⊃EF(TF(Q,Q0),TF(Q1,Q0))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF TF) . NIL . (FRACTMULT#9) . NIL . FRACTMULT . NIL . 9 .)(|∀Q Q1 Q0.LF(Q,Q1)⊃LF(TF(Q,Q0),TF(Q1,Q0))| . (AXIOM (TM& . |∀Q Q1 Q0.LF(Q,Q1)⊃LF(TF(Q,Q0),TF(Q1,Q0))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q LF TF) . NIL . (FRACTMULT#10) . NIL . FRACTMULT . NIL . 10 .)(|∀Q Q0 Q01.GF(TF(Q,Q01),TF(Q0,Q01))⊃GF(Q,Q0)| . (AXIOM (TM& . |∀Q Q0 Q01.GF(TF(Q,Q01),TF(Q0,Q01))⊃GF(Q,Q0)|)) . (M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q GF TF) . NIL . (FRACTMULT#11) . NIL . FRACTMULT . NIL . 11 .)(|∀Q Q0 Q01.EF(TF(Q,Q01),TF(Q0,Q01))⊃EF(Q,Q0)| . (AXIOM (TM& . |∀Q Q0 Q01.EF(TF(Q,Q01),TF(Q0,Q01))⊃EF(Q,Q0)|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF TF) . NIL . (FRACTMULT#12) . NIL . FRACTMULT . NIL . 12 .)(|∀Q Q0 Q01.LF(TF(Q,Q01),TF(Q0,Q01))⊃LF(Q,Q0)| . (AXIOM (TM& . |∀Q Q0 Q01.LF(TF(Q,Q01),TF(Q0,Q01))⊃LF(Q,Q0)|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q LF TF) . NIL . (FRACTMULT#13) . NIL . FRACTMULT . NIL . 13 .)(|∀Q Q1 Q0 Q01.GF(Q,Q1)∧GF(Q0,Q01)⊃GF(TF(Q,Q0),TF(Q1,Q01))| . (AXIOM (TM& . |∀Q Q1 Q0 Q01.GF(Q,Q1)∧GF(Q0,Q01)⊃GF(TF(Q,Q0),TF(Q1,Q01))|)) . (M N K J I ADD1 GREATERP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q GF TF) . NIL . (FRACTMULT#14) . NIL . FRACTMULT . NIL . 14 .)(|∀Q Q1 Q0 Q01.LEF(Q,Q1)∧LF(Q0,Q01)⊃LF(TF(Q,Q0),TF(Q1,Q01))| . (AXIOM (TM& . |∀Q Q1 Q0 Q01.LEF(Q,Q1)∧LF(Q0,Q01)⊃LF(TF(Q,Q0),TF(Q1,Q01))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF TF) . NIL . (FRACTMULT#15) . NIL . FRACTMULT . NIL . 15 .)(|∀Q Q1 Q0 Q01.LF(Q,Q1)∧LEF(Q0,Q01)⊃LF(TF(Q,Q0),TF(Q1,Q01))| . (AXIOM (TM& . |∀Q Q1 Q0 Q01.LF(Q,Q1)∧LEF(Q0,Q01)⊃LF(TF(Q,Q0),TF(Q1,Q01))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF TF) . NIL . (FRACTMULT#16) . NIL . FRACTMULT . NIL . 16 .)(|∀Q Q1 Q0 Q01.LEF(Q,Q1)∧LEF(Q0,Q01)⊃LEF(TF(Q,Q0),TF(Q1,Q01))| . (AXIOM (TM& . |∀Q Q1 Q0 Q01.LEF(Q,Q1)∧LEF(Q0,Q01)⊃LEF(TF(Q,Q0),TF(Q1,Q01))|)) . (M N K J I ADD1 LESSP TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF LF LEF TF) . NIL . (FRACTMULT#17) . NIL . FRACTMULT . NIL . 17 .)(|INV=(λQ.LIST(CADR(Q),CAR Q))| . (DEFINE INV (TM& . |INV=(λQ.LIST(CADR(Q),CAR Q))|) NIL) . (CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q (INV . (GROUND→GROUND . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRACTMULT#18 . NIL . DEFINED .))) . NIL . (FRACTMULT#18 MULTIP#10 LISPAX#30 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19 FRACTMULT#3) . NIL . FRACTMULT . NIL . 18 .)(|∀Q.¬QZEROP(Q)⊃FR(INV(Q))| . (AXIOM (TM& . |∀Q.¬QZEROP(Q)⊃FR(INV(Q))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF QZ QZEROP INV) . NIL . (FRACTMULT#19) . NIL . FRACTMULT . NIL . 19 .)(|∀Q.TF(Q,QONE)=Q| . (AXIOM (TM& . |∀Q.TF(Q,QONE)=Q|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q QONE TF) . NIL . (FRACTMULT#20) . NIL . FRACTMULT . NIL . 20 .)(|∀Q.TF(QONE,Q)=Q| . (AXIOM (TM& . |∀Q.TF(QONE,Q)=Q|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q QONE TF) . NIL . (FRACTMULT#21) . NIL . FRACTMULT . NIL . 21 .)(|∀Q.¬QZEROP(Q)⊃EF(TF(Q,INV(Q)),QONE)| . (AXIOM (TM& . |∀Q.¬QZEROP(Q)⊃EF(TF(Q,INV(Q)),QONE)|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF QZ QZEROP QONE TF INV) . NIL . (FRACTMULT#22) . NIL . FRACTMULT . NIL . 22 .)(|∀Q.EF(TF(Q,QZ),QZ)| . (AXIOM (TM& . |∀Q.EF(TF(Q,QZ),QZ)|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF QZ TF) . NIL . (FRACTMULT#23) . NIL . FRACTMULT . NIL . 23 .)(|∀Q0 Q.(∃Q1.¬QZEROP(Q)⊃EF(TF(Q,Q1),Q0))| . (AXIOM (TM& . |∀Q0 Q.(∃Q1.¬QZEROP(Q)⊃EF(TF(Q,Q1),Q0))|)) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF QZ QZEROP TF) . NIL . (FRACTMULT#24) . NIL . FRACTMULT . NIL . 24 .)(|∀Q Q0.¬QZEROP(Q)⊃EF(TF(Q,DIVIDED(Q0,Q)),Q0)| . (DEFINE DIVIDED (TM& . |∀Q Q0.¬QZEROP(Q)⊃EF(TF(Q,DIVIDED(Q0,Q)),Q0)|) ((USE (LR& FRACTMULT#24)) (USE (LR& SETS#9)))) . (M N K J I ADD1 TIMES PLUS CAR CDR SEXP LIST XV CADR FR Q03 Q02 Q01 Q3 Q2 Q1 Q0 Q EF QZ QZEROP TF (DIVIDED . (|(GROUND⊗GROUND)→GROUND| . (SYMBOL& UNIVERSAL NIL) . NIL . NIL . FRACTMULT#25 . NIL . DEFINED .))) . NIL . (FRACTMULT#25 MULTIP#10 LISPAX#30 FRACTMULT#24 SETS#9 NATNUM#5 NATNUM#6 NATNUM#7 NATNUM#14 NATNUM#13 NATNUM#16 NATNUM#17 NATNUM#24 NATNUM#25 NATNUM#26 NATNUM#27 NATNUM#28 ORDERING#9 ORDERING#14 ORDERING#21 MULTIP#2 MULTIP#3 MULTIP#4 LISPAX#13 LISPAX#14 LISPAX#15 LISPAX#16 LISPAX#17 LISPAX#18 LISPAX#19 LISPAX#20 LISPAX#21 LISPAX#22 LISPAX#23 LISPAX#24 LISPAX#25 LISPAX#26 LISPAX#27 LISPAX#28 LISPAX#29 LISPAX#43 LISPAX#44 LISPAX#45 LISPAX#47 LISPAX#48 LISPAX#49 LISPAX#50 LISPAX#56 LISPAX#58 LISPAX#61 LISPAX#66 LISPAX#67 LISPAX#70 LISPAX#71 LISPAX#73 LISPAX#74 LISPAX#75 LISPAX#76 FRACTIONS#2 FRACTIONS#3 FRACTIONS#4 FRACTIONS#5 MULTIP#11 FRACTIONS#6 FRACTIONS#9 FRORDERING#9 FRORDERING#29 FRORDERING#31 FRORDERING#33 FRACTSUM#3 FRACTSUM#19 FRACTMULT#3 FRACTMULT#19) . NIL . FRACTMULT . NIL . 25 .)